structure Lean.CollectLevelParams.State : Type

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

instance Lean.CollectLevelParams.instInhabitedState : Inhabited State

@[reducible, inline]

abbrev Lean.CollectLevelParams.Visitor : Type

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

partial def Lean.CollectLevelParams.collect : Level → Visitor

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

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

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

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