← Copula mathematical handbook

structure Lean.CollectFVars.State : Type

• visitedExpr : ExprSet
• fvarSet : FVarIdSet
• fvarIds : Array FVarId

@[instance_reducible]

instance Lean.CollectFVars.instInhabitedState : Inhabited State

Equations

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

def Lean.CollectFVars.State.add (s : State) (fvarId : FVarId) : State

Equations

• s.add fvarId = { visitedExpr := s.visitedExpr, fvarSet := s.fvarSet.insert fvarId, fvarIds := s.fvarIds.push fvarId }

@[reducible, inline]

abbrev Lean.CollectFVars.Visitor : Type

Equations

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

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

partial def Lean.CollectFVars.main : Expr → Visitor

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

Equations

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