structure Lean.CollectLevelParams.State : Type

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

instance Lean.CollectLevelParams.instInhabitedState : Inhabited State

Equations

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

@[reducible, inline]

abbrev Lean.CollectLevelParams.Visitor : Type

Equations

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

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

partial def Lean.CollectLevelParams.collect : Level → Visitor

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

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

partial def Lean.CollectLevelParams.main : Expr → Visitor

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

Equations

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

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

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

Equations

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

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

Equations

• s.collect e = Lean.collectLevelParams s e