partial def Lean.Meta.collectMVars (e : Expr) : StateRefT' IO.RealWorld CollectMVars.State MetaM Unit

Collect unassigned metavariables occurring 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.

def Lean.Meta.getMVars (e : Expr) : MetaM (Array MVarId)

Return metavariables occurring in the given expression. See collectMVars

Equations

• Lean.Meta.getMVars e = do let __discr ← (Lean.Meta.collectMVars e).run { } match __discr with | (fst, s) => pure s.result

def Lean.Meta.getMVarsNoDelayed (e : Expr) : MetaM (Array MVarId)

Similar to getMVars, but removes delayed assignments.

Equations

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

def Lean.Meta.collectMVarsAtDecl (d : Declaration) : StateRefT' IO.RealWorld CollectMVars.State MetaM Unit

Equations

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

def Lean.Meta.getMVarsAtDecl (d : Declaration) : MetaM (Array MVarId)

Equations

• Lean.Meta.getMVarsAtDecl d = do let __discr ← (Lean.Meta.collectMVarsAtDecl d).run { } match __discr with | (fst, s) => pure s.result

def Lean.MVarId.getMVarDependencies (mvarId : MVarId) (includeDelayed : Bool := false) : MetaM (Std.HashSet MVarId)

Collect the metavariables which mvarId depends on. These are the metavariables which appear in the type and local context of mvarId, as well as the metavariables which those metavariables depend on, etc.

Equations

• mvarId.getMVarDependencies includeDelayed = (fun (x : Unit × Std.HashSet Lean.MVarId) => x.snd) <$> (go✝ mvarId includeDelayed).run ∅

def Lean.Expr.getMVarDependencies (e : Expr) (includeDelayed : Bool := false) : MetaM (Std.HashSet MVarId)

Collect the metavariables appearing in the expression e, including metavariables in the type or local context of any such metavariables, etc.

Equations

• e.getMVarDependencies includeDelayed = (fun (x : Unit × Std.HashSet Lean.MVarId) => x.snd) <$> (addMVars✝ e includeDelayed).run ∅