Documentation

Lean.Meta.AbstractMVars

structure Lean.Meta.AbstractMVarsResult:

Type

paramNames : Array Lean.Name
numMVars : Nat
expr : Lean.Expr

instance Lean.Meta.instInhabitedAbstractMVarsResult:

Inhabited Lean.Meta.AbstractMVarsResult

Equations

Lean.Meta.instInhabitedAbstractMVarsResult = { default := { paramNames := default, numMVars := default, expr := default } }

instance Lean.Meta.instBEqAbstractMVarsResult:

BEq Lean.Meta.AbstractMVarsResult

Equations

Lean.Meta.instBEqAbstractMVarsResult = { beq := [anonymous] }

structure Lean.Meta.AbstractMVars.State:

Type

ngen : Lean.NameGenerator
lctx : Lean.LocalContext
mctx : Lean.MetavarContext
nextParamIdx : Nat
paramNames : Array Lean.Name
fvars : Array Lean.Expr
lmap : Std.HashMap Lean.MVarId Lean.Level
emap : Std.HashMap Lean.MVarId Lean.Expr

@[inline]

abbrev Lean.Meta.AbstractMVars.M (α : Type) :

Type

Equations

Lean.Meta.AbstractMVars.M = StateM Lean.Meta.AbstractMVars.State

def Lean.Meta.AbstractMVars.mkFreshId:

Lean.Meta.AbstractMVars.M Lean.Name

Equations

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

def Lean.Meta.AbstractMVars.mkFreshFVarId:

Lean.Meta.AbstractMVars.M Lean.FVarId

Equations

Lean.Meta.AbstractMVars.mkFreshFVarId = do let a ← Lean.Meta.AbstractMVars.mkFreshId pure { name := a }

partial def Lean.Meta.AbstractMVars.abstractExprMVars (e : Lean.Expr) :

Lean.Meta.AbstractMVars.M Lean.Expr

def Lean.Meta.abstractMVars (e : Lean.Expr) :

Lean.MetaM Lean.Meta.AbstractMVarsResult

Abstract (current depth) metavariables occurring in e. The result contains

An array of universe level parameters that replaced universe metavariables occurring in e.
The number of (expr) metavariables abstracted.
And an expression of the form fun (m_1 : A_1) ... (m_k : A_k) => e', where k equal to the number of (expr) metavariables abstracted, and e' is e after we replace the metavariables.

Example: given f.{?u} ?m1 where ?m1 : ?m2 Nat, ?m2 : Type -> Type. This function returns { levels := #[u], size := 2, expr := (fun (m2 : Type -> Type) (m1 : m2 Nat) => f.{u} m1) }

This API can be used to "transport" to a different metavariable context. Given a new metavariable context, we replace the AbstractMVarsResult.levels with new fresh universe metavariables, and instantiate the (m_i : A_i) in the lambda-expression with new fresh metavariables.

Application: we use this method to cache the results of type class resolution.

Equations

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

def Lean.Meta.openAbstractMVarsResult (a : Lean.Meta.AbstractMVarsResult) :

Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)

Equations

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