def Lean.Expr.collectFVars (e : Lean.Expr) : StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit

Equations

• e.collectFVars = do let e ← Lean.instantiateMVars e modify fun (used : Lean.CollectFVars.State) => Lean.collectFVars used e

def Lean.LocalDecl.collectFVars (localDecl : Lean.LocalDecl) : StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit

Equations

• (Lean.LocalDecl.cdecl index fvarId userName type bi kind).collectFVars = type.collectFVars
• (Lean.LocalDecl.ldecl index fvarId userName type value nonDep kind).collectFVars = do type.collectFVars value.collectFVars

def Lean.CollectFVars.State.addDependencies (s : Lean.CollectFVars.State) : Lean.MetaM Lean.CollectFVars.State

For each variable in s.fvarSet, include its dependencies.

Equations

• s.addDependencies = do let __discr ← (Lean.CollectFVars.State.addDependencies.go.run 0).run s match __discr with | (fst, s) => pure s

def Lean.CollectFVars.State.addDependencies.getNext? : StateRefT' IO.RealWorld Nat (StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM) (Option Lean.FVarId)

Equations

• One or more equations did not get rendered due to their size.

partial def Lean.CollectFVars.State.addDependencies.go : StateRefT' IO.RealWorld Nat (StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM) Unit

def Lean.Meta.removeUnused (vars : Array Lean.Expr) (used : Lean.CollectFVars.State) : Lean.MetaM (Lean.LocalContext × Lean.LocalInstances × Array Lean.Expr)

Equations

• One or more equations did not get rendered due to their size.