Documentation

Lean.Util.CollectMVars

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]

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