Expand description
Universe levels: hash-consed, with a COMPLETE decision procedure for ≤ and ≡.
Lean’s C++ kernel decides level equality by a normalisation that is sound but incomplete, and
two of the Arena’s soundness tests (level-imax-leq, level-imax-normalization) exist because
an earlier version of it was unsound. Here u ≤ v is decided exactly — “for every assignment
of natural numbers to the parameters” — by case analysis on the only non-monotone operator:
imax u v is 0 when v = 0 and max u v otherwise. A parameter that can make an imax
right side vanish is split into p = 0 and p = p' + 1; once no imax can vanish, both
sides are max(c, p₁+k₁, …) and comparison is a closed-form check.
Structs§
- LevelId
- Levels
- Levels
Id - An interned list of levels (the universe arguments of a constant).
- SubstId
- A universe substitution — a constant’s level parameters replaced by the levels of one use of it — interned, so that a value can carry it as one id.