Documentation

Lean.Meta.CollectMVars

partial def Lean.Meta.collectMVars (e : Lean.Expr) :

StateRefT' IO.RealWorld Lean.CollectMVars.State Lean.MetaM Unit

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

Lean.MetaM (Array Lean.MVarId)

Equations

Lean.Meta.getMVars e = do let discr ← StateRefT'.run (Lean.Meta.collectMVars e) { visitedExpr := ∅, result := #[] } let x : Unit × Lean.CollectMVars.State := discr match x with | (x, s) => pure s.result

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

Lean.MetaM (Array Lean.MVarId)

Equations

Lean.Meta.getMVarsNoDelayed e = do let mvarIds ← Lean.Meta.getMVars e Array.filterM (fun mvarId => not <$> Lean.Meta.isDelayedAssigned mvarId) mvarIds 0 (Array.size mvarIds)

def Lean.Meta.collectMVarsAtDecl (d : Lean.Declaration) :

StateRefT' IO.RealWorld Lean.CollectMVars.State Lean.MetaM Unit

Equations

Lean.Meta.collectMVarsAtDecl d = Lean.Declaration.forExprM d Lean.Meta.collectMVars

def Lean.Meta.getMVarsAtDecl (d : Lean.Declaration) :

Lean.MetaM (Array Lean.MVarId)

Equations

Lean.Meta.getMVarsAtDecl d = do let discr ← StateRefT'.run (Lean.Meta.collectMVarsAtDecl d) { visitedExpr := ∅, result := #[] } let x : Unit × Lean.CollectMVars.State := discr match x with | (x, s) => pure s.result