structure Lean.Meta.AbstractMVarsResult : Type

• paramNames : Array Lake.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 := Lean.Meta.beqAbstractMVarsResult✝ }

structure Lean.Meta.AbstractMVars.State : Type

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

@[inline, reducible]

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

Equations

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

@[always_inline]

instance Lean.Meta.AbstractMVars.instMonadMCtxM : Lean.MonadMCtx Lean.Meta.AbstractMVars.M

Equations

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

def Lean.Meta.AbstractMVars.mkFreshId : Lean.Meta.AbstractMVars.M Lake.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 __do_lift ← Lean.Meta.AbstractMVars.mkFreshId pure { name := __do_lift }

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.