Documentation

Lean.Util.CollectLevelParams

structure Lean.CollectLevelParams.State:

Type

visitedLevel : Lean.LevelSet
visitedExpr : Lean.ExprSet
params : Array Lean.Name

instance Lean.CollectLevelParams.instInhabitedState:

Inhabited Lean.CollectLevelParams.State

Equations

Lean.CollectLevelParams.instInhabitedState = { default := { visitedLevel := ∅, visitedExpr := ∅, params := #[] } }

@[inline]

abbrev Lean.CollectLevelParams.Visitor:

Type

Equations

Lean.CollectLevelParams.Visitor = (Lean.CollectLevelParams.State → Lean.CollectLevelParams.State)

partial def Lean.CollectLevelParams.visitLevel (u : Lean.Level) :

Lean.CollectLevelParams.Visitor

partial def Lean.CollectLevelParams.collect:

Lean.Level → Lean.CollectLevelParams.Visitor

partial def Lean.CollectLevelParams.visitExpr (e : Lean.Expr) :

Lean.CollectLevelParams.Visitor

partial def Lean.CollectLevelParams.main:

Lean.Expr → Lean.CollectLevelParams.Visitor

def Lean.CollectLevelParams.State.getUnusedLevelParam (s : Lean.CollectLevelParams.State) (pre : optParam Lean.Name `v) :

Equations

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

partial def Lean.CollectLevelParams.State.getUnusedLevelParam.loop (s : Lean.CollectLevelParams.State) (pre : optParam Lean.Name `v) (i : Nat) :

def Lean.collectLevelParams (s : Lean.CollectLevelParams.State) (e : Lean.Expr) :

Lean.CollectLevelParams.State

Equations

Lean.collectLevelParams s e = Lean.CollectLevelParams.main e s

def Lean.CollectLevelParams.State.collect (s : Lean.CollectLevelParams.State) (e : Lean.Expr) :

Lean.CollectLevelParams.State

Equations

Lean.CollectLevelParams.State.collect s e = Lean.collectLevelParams s e