Method offset

crates/kernel/src/level.rs:116–128

Peel the outermost constant offset: returns `(base, n)` where `self = Succ^n(base)` and `base` is not `Succ`.

(&self)

  }

  /// True if this level is an explicit numeral: `Succ^n(Zero)` for some n ≥ 0.
  pub fn is_explicit(&self) -> bool {
    match self.data() {
      UnivData::Zero(_) => true,
      UnivData::Succ(inner, _) => inner.is_explicit(),
      _ => false,
    }
  }

  /// True if this level is `Succ^n(base)` with n > 0. Such a level is never
  /// zero under any parameter assignment.
  pub fn is_never_zero(&self) -> bool {
    match self.data() {
      UnivData::Succ(..) => true,
      UnivData::Max(a, b, _) => a.is_never_zero() || b.is_never_zero(),
      UnivData::IMax(_, b, _) => b.is_never_zero(),