structure Lean.CollectFVars.State : Type

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

instance Lean.CollectFVars.instInhabitedState : Inhabited Lean.CollectFVars.State

Equations

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

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

Equations

• Lean.CollectFVars.State.add s fvarId = { visitedExpr := s.visitedExpr, fvarSet := Lean.FVarIdSet.insert s.fvarSet fvarId, fvarIds := Array.push s.fvarIds fvarId }

@[inline, reducible]

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