ToLevel
class #
This module defines Lean.ToLevel
, which is the Lean.Level
analogue to Lean.ToExpr
.
A class to create Level
expressions that denote particular universe levels in Lean.
Lean.ToLevel.toLevel.{u}
evaluates to a Lean.Level
term representing u
- toLevel : Level
A
Level
that represents the universe levelu
. A hack to avoid the "unused universe parameter" error. We can remove this field pending issue https://github.com/leanprover/lean4/issues/2116