Documentation

Lean.Meta.CollectFVars

def Lean.Expr.collectFVars (e : Lean.Expr) :

StateRefT' IO.RealWorld Lean.CollectFVars.State Lean.MetaM Unit

Equations

Lean.Expr.collectFVars e = do let e ← liftM (Lean.Meta.instantiateMVars e) modify fun used => 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.