structure Duper.AbstractMVars.AbstractMVarsResult : Type

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

instance Duper.AbstractMVars.instInhabitedAbstractMVarsResult : Inhabited AbstractMVarsResult

Equations

• Duper.AbstractMVars.instInhabitedAbstractMVarsResult = { default := { paramNames := default, numMVars := default, expr := default } }

instance Duper.AbstractMVars.instBEqAbstractMVarsResult : BEq AbstractMVarsResult

Equations

• Duper.AbstractMVars.instBEqAbstractMVarsResult = { beq := Duper.AbstractMVars.beqAbstractMVarsResult✝ }

structure Duper.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.LMVarId Lean.Level
• emap : Std.HashMap Lean.MVarId Lean.Expr

@[reducible, inline]

abbrev Duper.AbstractMVars.M (α : Type) : Type

Equations

• Duper.AbstractMVars.M = StateM Duper.AbstractMVars.State

@[always_inline]

instance Duper.AbstractMVars.instMonadMCtxM : Lean.MonadMCtx M

Equations

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

def Duper.AbstractMVars.mkFreshId : M Lean.Name

Equations

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

def Duper.AbstractMVars.mkFreshFVarId : M Lean.FVarId

Equations

• Duper.AbstractMVars.mkFreshFVarId = do let __do_lift ← Duper.AbstractMVars.mkFreshId pure { name := __do_lift }

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

def Duper.abstractMVars (e : Lean.Expr) : Lean.MetaM AbstractMVars.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 Duper.openAbstractMVarsResult (a : AbstractMVars.AbstractMVarsResult) : Lean.MetaM (Array Lean.Expr × Array Lean.BinderInfo × Lean.Expr)

Equations

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

def Duper.abstractMVarsForall (e : Lean.Expr) : Lean.MetaM AbstractMVars.AbstractMVarsResult

Equations

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

def Duper.abstractMVarsLambdaWithIds (e : Lean.Expr) : Lean.MetaM (Lean.Expr × Array Lean.Expr × Array Lean.Name × Array Lean.Level)

Equations

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

def Duper.abstractMVarsLambda (e : Lean.Expr) : Lean.MetaM AbstractMVars.AbstractMVarsResult

Equations

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