Method succ

crates/kernel/src/level.rs:136–141

(inner: KUniv<M>)

  }

  /// Peel the outermost constant offset: returns `(base, n)` where
  /// `self = Succ^n(base)` and `base` is not `Succ`.
  pub fn offset(&self) -> (&KUniv<M>, u64) {
    let mut u = self;
    let mut n = 0u64;
    loop {
      match u.data() {
        UnivData::Succ(inner, _) => {
          u = inner;