Expand description
Universe levels for Lean’s predicative type theory
Implements universe levels: 0, 1, 2, …, u+1, max(u,v), imax(u,v)
Structs§
- Level
Arena - Arena for interning universe levels
- LevelId
- Interned universe level ID
Enums§
- Level
- Universe level expressions