def Lean.Meta.Sym.lowerLooseBVarsS' (e : Expr) (s d : Nat) : Internal.AlphaShareBuilderM Expr

Lowers the loose bound variables >= s in e by d. That is, a loose bound variable bvar i with i >= s is mapped to bvar (i-d). It assumes the input is maximally shared, and ensures the output is too. Remark: if s < d, then the result is e.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Sym.lowerLooseBVarsS (e : Expr) (s d : Nat) : SymM Expr

Lowers the loose bound variables >= s in e by d. That is, a loose bound variable bvar i with i >= s is mapped to bvar (i-d). It assumes the input is maximally shared, and ensures the output is too. Remark: if s < d, then the result is e.

Equations

• Lean.Meta.Sym.lowerLooseBVarsS e s d = Lean.Meta.Sym.Internal.liftBuilderM (Lean.Meta.Sym.lowerLooseBVarsS' e s d)

def Lean.Meta.Sym.liftLooseBVarsS' (e : Expr) (s d : Nat) : Internal.AlphaShareBuilderM Expr

Lifts loose bound variables >= s in e by d. It assumes the input is maximally shared, and ensures the output is too.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Meta.Sym.liftLooseBVarsS (e : Expr) (s d : Nat) : SymM Expr

Lifts loose bound variables >= s in e by d. It assumes the input is maximally shared, and ensures the output is too.

Equations

• Lean.Meta.Sym.liftLooseBVarsS e s d = Lean.Meta.Sym.Internal.liftBuilderM (Lean.Meta.Sym.liftLooseBVarsS' e s d)