Method is_explicit

crates/kernel/src/level.rs:95–101

True if this level is an explicit numeral: `Succ^n(Zero)` for some n ≥ 0.

(&self)

  /// names are NOT compared (matching the historical hash semantics).
  /// Equal interned subtrees prune at the uid fast path.
  fn structural_eq(&self, other: &Self) -> bool {
    if self.hash_eq(other) {
      return true;
    }
    match (self.data(), other.data()) {
      (UnivData::Zero(_), UnivData::Zero(_)) => true,
      (UnivData::Succ(a, _), UnivData::Succ(b, _)) => a.structural_eq(b),
      (UnivData::Max(a1, b1, _), UnivData::Max(a2, b2, _))
      | (UnivData::IMax(a1, b1, _), UnivData::IMax(a2, b2, _)) => {
        a1.structural_eq(a2) && b1.structural_eq(b2)