Documentation

Lean.Meta.Sym.InstantiateS

source
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

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[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.

    Equations
    Instances For
      source
      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.

      Equations
      Instances For
        source
        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.

        Equations
        Instances For