structure Lean.CollectLevelParams.State : Type

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

instance Lean.CollectLevelParams.instInhabitedState : Inhabited Lean.CollectLevelParams.State

Equations

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

@[inline, reducible]

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

def Lean.CollectLevelParams.visitLevels (us : List Lean.Level) : Lean.CollectLevelParams.Visitor

Equations

• Lean.CollectLevelParams.visitLevels us s = List.foldl (fun s u => Lean.CollectLevelParams.visitLevel u s) s us

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 Lake.Name `v) : Lean.Level

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 Lake.Name `v) (i : Nat) : Lean.Level

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