Documentation

Lean.Util.CollectFVars

structure Lean.CollectFVars.State :

Type

visitedExpr : Lean.ExprSet
fvarSet : Lean.FVarIdSet

instance Lean.CollectFVars.instInhabitedState :

Inhabited Lean.CollectFVars.State

Equations

Lean.CollectFVars.instInhabitedState = { default := { visitedExpr := default, fvarSet := default } }

@[inline]

abbrev Lean.CollectFVars.Visitor :

Type

Equations

Lean.CollectFVars.Visitor = (Lean.CollectFVars.State → Lean.CollectFVars.State)

partial def Lean.CollectFVars.visit (e : Lean.Expr) :

Lean.CollectFVars.Visitor

partial def Lean.CollectFVars.main :

Lean.Expr → Lean.CollectFVars.Visitor

def Lean.collectFVars (s : Lean.CollectFVars.State) (e : Lean.Expr) :

Lean.CollectFVars.State

Equations

Lean.collectFVars s e = Lean.CollectFVars.main e s