def Lean.Expr.collectFVars (e : Expr) : StateRefT' IO.RealWorld CollectFVars.State 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 : LocalDecl) : StateRefT' IO.RealWorld CollectFVars.State 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 : State) : MetaM 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 State MetaM) (Option 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 State MetaM) Unit

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

Equations

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