structure Lean.Meta.AbstractMVars.State : Type

• ngen : NameGenerator
• lctx : LocalContext
• mctx : MetavarContext
• nextParamIdx : Nat
• paramNames : Array Name
• fvars : Array Expr
• mvars : Array Expr
• lmap : Std.HashMap LMVarId Level
• emap : Std.HashMap MVarId Expr
• abstractLevels : Bool

@[reducible, inline]

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

@[always_inline]

instance Lean.Meta.AbstractMVars.instMonadMCtxM : MonadMCtx M

def Lean.Meta.AbstractMVars.mkFreshId : M Name

def Lean.Meta.AbstractMVars.mkFreshFVarId : M FVarId

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

def Lean.Meta.abstractMVars (e : Expr) (levels : Bool := true) : MetaM 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 metavariables that have been 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.

If levels := false, then level metavariables are not abstracted.

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

Application: tactic MVarId.abstractMVars

def Lean.Meta.openAbstractMVarsResult (a : AbstractMVarsResult) : MetaM (Array Expr × Array BinderInfo × Expr)