Method is_never_zero

crates/kernel/src/level.rs:105–112

True if this level is `Succ^n(base)` with n > 0. Such a level is never zero under any parameter assignment.

(&self)

      | (UnivData::IMax(a1, b1, _), UnivData::IMax(a2, b2, _)) => {
        a1.structural_eq(a2) && b1.structural_eq(b2)
      },
      (UnivData::Param(i, _, _), UnivData::Param(j, _, _)) => i == j,
      _ => false,
    }
  }

  /// True if this level is definitionally zero (Prop).
  pub fn is_zero(&self) -> bool {
    matches!(self.data(), UnivData::Zero(_))
  }