structure Lean.CollectMVars.State : Type

• visitedExpr : ExprSet
• result : Array MVarId

Instances For

• Lean.CollectMVars.instInhabitedState

instance Lean.CollectMVars.instInhabitedState : Inhabited State

Equations

• Lean.CollectMVars.instInhabitedState = { default := { visitedExpr := ∅, result := #[] } }

@[reducible, inline]

abbrev Lean.CollectMVars.Visitor : Type

Equations

• Lean.CollectMVars.Visitor = (Lean.CollectMVars.State → Lean.CollectMVars.State)

partial def Lean.CollectMVars.visit (e : Expr) : Visitor

partial def Lean.CollectMVars.main : Expr → Visitor

def Lean.Expr.collectMVars (s : CollectMVars.State) (e : Expr) : CollectMVars.State

Equations

• Lean.Expr.collectMVars s e = Lean.CollectMVars.visit e s