source
structure Lean.CollectLevelParams.State :
Type

- visitedLevel : LevelSet
- visitedExpr : ExprSet
- params : Array Name

Instances For

source
instance Lean.CollectLevelParams.instInhabitedState :
Inhabited State
Equations

- Lean.CollectLevelParams.instInhabitedState = { default := { } }

source
@[reducible, inline]
abbrev Lean.CollectLevelParams.Visitor :
Type
Equations

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

Instances For

source
partial def Lean.CollectLevelParams.visitLevel (u : Level) :
Visitor
source
partial def Lean.CollectLevelParams.collect :
Level → Visitor
source
def Lean.CollectLevelParams.visitLevels (us : List Level) :
Visitor
Equations

- Lean.CollectLevelParams.visitLevels us s = List.foldl (fun (s : Lean.CollectLevelParams.State) (u : Lean.Level) => Lean.CollectLevelParams.visitLevel u s) s us

Instances For

source
partial def Lean.CollectLevelParams.visitExpr (e : Expr) :
Visitor
source
partial def Lean.CollectLevelParams.main :
Expr → Visitor
source
def Lean.CollectLevelParams.State.getUnusedLevelParam (s : State) (pre : Name := `v) :
Level
Equations

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

Instances For

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

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

Instances For

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

- s.collect e = Lean.collectLevelParams s e

Instances For