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.

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.

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.

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.