def Lean.Meta.Sym.abstractFVarsRange (e : Expr) (start : Nat) (xs : Array Expr) : SymM Expr

Abstracts free variables xs[start...*] in expression e, converting them to de Bruijn indices.

Assumptions:

• The local context of the metavariables occurring in e do not include the free variables being abstracted. This invariant holds when abstracting over binders during pattern matching/unification: metavariables in the pattern were created before entering the binder, so their contexts exclude the bound variable's corresponding fvar.

• If xs[start...*] is not empty, then the minimal variable is xs[start].

• Subterms whose maxFVar is below minFVarId are skipped entirely. This function does not assume the maxFVar cache contains information for every subterm in e.

Equations

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

@[reducible, inline]

abbrev Lean.Meta.Sym.abstractFVars (e : Expr) (xs : Array Expr) : SymM Expr

Abstracts free variables xs in expression e, converting them to de Bruijn indices.

It is an abbreviation for abstractFVarsRange e 0 xs.

Equations

• Lean.Meta.Sym.abstractFVars e xs = Lean.Meta.Sym.abstractFVarsRange e 0 xs

def Lean.Meta.Sym.mkLambdaFVarsS (xs : Array Expr) (e : Expr) : SymM Expr

Similar to mkLambdaFVars, but uses the more efficient abstractFVars and abstractFVarsRange, and makes the same assumption made by these functions.

Equations

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

def Lean.Meta.Sym.mkForallFVarsS (xs : Array Expr) (e : Expr) : SymM Expr

Similar to mkForallFVars, but uses the more efficient abstractFVars and abstractFVarsRange, and makes the same assumption made by these functions.

Equations

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