structure Lean.CollectMVars.State : Type

• visitedExpr : Lean.ExprSet
• result : Array Lean.MVarId

instance Lean.CollectMVars.instInhabitedState : Inhabited Lean.CollectMVars.State

Equations

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

@[inline, reducible]

abbrev Lean.CollectMVars.Visitor : Type

Equations

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

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

partial def Lean.CollectMVars.main : Lean.Expr → Lean.CollectMVars.Visitor

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

Equations

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