ToLevel
class #
This module defines Lean.ToLevel
, which is the Lean.Level
analogue to Lean.ToExpr
.
Warning: Import Mathlib.Tactic.ToExpr
instead of this one if you are writing ToExpr
instances. This ensures that you are using the universe polymorphic ToExpr
instances that
override the ones from Lean 4 core.
- toLevel : Lean.Level
A
Level
that represents the universe levelu
. - univ : Type u
The universe itself. This is only here to avoid the "unused universe parameter" error.
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