Lean.Meta.CollectMVars

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

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

Collect unassigned metavariables occuring in the given expression.

Remark: if e contains ?m and there is a t assigned to ?m, we collect unassigned metavariables occurring in t.

Remark: if e contains ?m and ?m is delayed assigned to some term t, we collect ?m and unassigned metavariables occurring in t. We collect ?m because it has not been assigned yet.

source

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

Lean.MetaM (Array Lean.MVarId)

Return metavariables in occuring the given expression. See collectMVars

Equations

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

source

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

Lean.MetaM (Array Lean.MVarId)

Similar to getMVars, but removes delayed assignments.

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)

source

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

source

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 := #[] } match discr with | (fst, s) => pure s.result