← Copula mathematical handbook

structure Lean.CollectMVars.State : Type

• visitedExpr : ExprSet
• result : Array MVarId

@[instance_reducible]

instance Lean.CollectMVars.instInhabitedState : Inhabited State

Equations

• Lean.CollectMVars.instInhabitedState = { default := { } }

@[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