partial def Lean.Meta.collectMVars (e : Lean.Expr) : StateRefT' IO.RealWorld Lean.CollectMVars.State Lean.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 : Lean.Expr) : Lean.MetaM (Array Lean.MVarId)

Return metavariables occurring in 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

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 : Lean.MVarId) => not <$> Lean.MVarId.isDelayedAssigned mvarId) mvarIds 0

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

def Lean.MVarId.getMVarDependencies (mvarId : Lean.MVarId) (includeDelayed : optParam Bool false) : Lean.MetaM (Lean.HashSet Lean.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

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

partial def Lean.MVarId.getMVarDependencies.addMVars (includeDelayed : optParam Bool false) (e : Lean.Expr) : StateRefT' IO.RealWorld (Lean.HashSet Lean.MVarId) Lean.MetaM Unit

Auxiliary definition for getMVarDependencies.

partial def Lean.MVarId.getMVarDependencies.go (includeDelayed : optParam Bool false) (mvarId : Lean.MVarId) : StateRefT' IO.RealWorld (Lean.HashSet Lean.MVarId) Lean.MetaM Unit

Auxiliary definition for getMVarDependencies.