Documentation

Lean.Meta.AbstractMVars

structure Lean.Meta.AbstractMVarsResult :

Type

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

instance Lean.Meta.instBEqAbstractMVarsResult :

BEq Lean.Meta.AbstractMVarsResult

Equations

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

instance Lean.Meta.instInhabitedAbstractMVarsResult :

Inhabited Lean.Meta.AbstractMVarsResult

Equations

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

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

Lean.Meta.AbstractMVars.mkFreshId = do let s ← get let fresh : Lean.Name := Lean.NameGenerator.curr s.ngen modify fun s => { ngen := Lean.NameGenerator.next s.ngen, lctx := s.lctx, mctx := s.mctx, nextParamIdx := s.nextParamIdx, paramNames := s.paramNames, fvars := s.fvars, lmap := s.lmap, emap := s.emap } pure fresh

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

Equations

Lean.Meta.abstractMVars e = do let e ← Lean.Meta.instantiateMVars e let a ← Lean.getMCtx let a_1 ← Lean.getLCtx let a_2 ← Lean.getNGen let x : Id (Lean.Expr × Lean.Meta.AbstractMVars.State) := Lean.Meta.AbstractMVars.abstractExprMVars e { ngen := a_2, lctx := a_1, mctx := a, nextParamIdx := 0, paramNames := #[], fvars := #[], lmap := ∅, emap := ∅ } match x with | (e, s) => do Lean.setNGen s.ngen Lean.Meta.setMCtx s.mctx let e : Lean.Expr := Lean.LocalContext.mkLambda s.lctx s.fvars e pure { paramNames := s.paramNames, numMVars := Array.size s.fvars, expr := e }

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

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

Equations

Lean.Meta.openAbstractMVarsResult a = do let us ← Array.mapM (fun x => Lean.Meta.mkFreshLevelMVar) a.paramNames let e : Lean.Expr := Lean.Expr.instantiateLevelParamsArray a.expr a.paramNames us Lean.Meta.lambdaMetaTelescope e (some a.numMVars)