def Lean.Meta.Sym.instantiateRevRangeS (e : Expr) (beginIdx endIdx : Nat) (subst : Array Expr) : SymM Expr

Similar to Lean.Expr.instantiateRevRange. It assumes the input is maximally shared, and ensures the output is too. It assumes beginIdx ≤ endIdx and endIdx ≤ subst.size

@[inline]

def Lean.Meta.Sym.instantiateRevS (e : Expr) (subst : Array Expr) : SymM Expr

Similar to Lean.Expr.instantiateRev. It assumes the input is maximally shared, and ensures the output is too.

def Lean.Meta.Sym.instantiateS (e : Expr) (subst : Array Expr) : SymM Expr

Similar to Lean.Expr.instantiate. It assumes the input is maximally shared, and ensures the output is too.

def Lean.Meta.Sym.instantiateRevBetaS (e : Expr) (subst : Array Expr) : SymM Expr

Similar to instantiateRevS, but beta-reduces nested applications whose function becomes a lambda after substitution.

For example, if e contains a subterm #0 a and we apply the substitution #0 := fun x => x + 1, then instantiateRevBetaS produces a + 1 instead of (fun x => x + 1) a.

This is useful when applying theorems. For example, when applying Exists.intro:

Exists.intro.{u} {α : Sort u} {p : α → Prop} (w : α) (h : p w) : Exists p

to a goal of the form ∃ x : Nat, p x ∧ q x, we create metavariables ?w and ?h. With instantiateRevBetaS, the type of ?h becomes p ?w ∧ q ?w instead of (fun x => p x ∧ q x) ?w.

def Lean.Meta.Sym.betaRevS (f : Expr) (revArgs : Array Expr) : SymM Expr

Beta-reduces f applied to reversed arguments revArgs, ensuring maximally shared terms. betaRevS f #[a₃, a₂, a₁] computes the beta-normal form of f a₁ a₂ a₃.

def Lean.Meta.Sym.betaS (f : Expr) (args : Array Expr) : SymM Expr

Apply the given arguments to f, beta-reducing if f is a lambda expression, ensuring maximally shared terms. See betaRevS for details.