Method imax

crates/common/src/env.rs:427–433

Constructs `imax x y` (impredicative max).

(x: Level, y: Level)

    let mut n: u64 = 0;
    while let LevelData::Succ(inner, _) = cur.as_data() {
      n += 1;
      cur = inner.clone();
    }
    (cur, n)
  }
  /// If this level is an explicit numeral `Succ^n(Zero)`, returns
  /// `Some((Zero, n))`. Otherwise returns `None`.
  pub fn explicit_offset(&self) -> Option<(Level, u64)> {
    let (base, n) = self.peel_succ();
    if matches!(base.as_data(), LevelData::Zero(_)) {