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

Equations

• Lean.Expr.collectFVars e = 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

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

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

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

Equations

• Lean.CollectFVars.State.addDependencies s = do let __discr ← StateRefT'.run (StateRefT'.run Lean.CollectFVars.State.addDependencies.go 0) 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.