Normalize a level by applying `Level::max_smart` / `Level::imax_smart` bottom-up. Idempotent. `Succ` is left raw (see [`level_alpha_eq`]).
(l: &Level)
| 45 | /// Normalize a level by applying `Level::max_smart` / `Level::imax_smart` |
| 46 | /// bottom-up. Idempotent. `Succ` is left raw (see [`level_alpha_eq`]). |
| 47 | fn normalize_level(l: &Level) -> Level { |
| 48 | match l.as_data() { |
| 49 | LevelData::Zero(_) | LevelData::Param(_, _) | LevelData::Mvar(_, _) => { |
| 50 | l.clone() |
| 51 | }, |
| 52 | LevelData::Succ(inner, _) => Level::succ(normalize_level(inner)), |
| 53 | LevelData::Max(x, y, _) => { |
| 54 | Level::max_smart(normalize_level(x), normalize_level(y)) |
| 55 | }, |
| 56 | LevelData::Imax(x, y, _) => { |
| 57 | Level::imax_smart(normalize_level(x), normalize_level(y)) |
| 58 | }, |
| 59 | } |
| 60 | } |
| 61 | |
| 62 | /// Strict structural alpha-equivalence on already-normalized levels. |
| 63 | /// Direct callers should go through [`level_alpha_eq`] so both sides |