Method max

crates/kernel/src/level.rs:153–191

Construct `max(a, b)` with Lean-style simplifications: - `max(k₁, k₂) = max(k₁, k₂)` when both are explicit numerals - `max(a, a) = a` - `max(0, a) = a`, `max(a, 0) = a` - `max(a, max(a, b)) = max(a, b)` (absorption) - `max(max(a, b), b) = max(a, b)` (absorption) - `max(succ^n(base), succ^m(base)) = succ^max(n,m)(base)` (same-base offset) Matches Lean's `mk_max` in `kernel/level.cpp:81-103`.

(a: KUniv<M>, b: KUniv<M>)

}

impl<M: KernelMode> KUniv<M> {
  pub fn zero() -> Self {
    KUniv::new(UnivData::Zero(super::expr::fresh_uid()))
  }

  pub fn succ(inner: KUniv<M>) -> Self {
    KUniv::new(UnivData::Succ(inner, super::expr::fresh_uid()))
  }

  /// Construct `max(a, b)` with Lean-style simplifications:
  ///
  /// - `max(k₁, k₂) = max(k₁, k₂)` when both are explicit numerals
  /// - `max(a, a) = a`
  /// - `max(0, a) = a`, `max(a, 0) = a`
  /// - `max(a, max(a, b)) = max(a, b)` (absorption)
  /// - `max(max(a, b), b) = max(a, b)` (absorption)
  /// - `max(succ^n(base), succ^m(base)) = succ^max(n,m)(base)` (same-base offset)
  ///
  /// Matches Lean's `mk_max` in `kernel/level.cpp:81-103`.
  pub fn max(a: KUniv<M>, b: KUniv<M>) -> Self {
    // Both explicit numerals (Succ^n(Zero)): take the larger.
    if a.is_explicit() && b.is_explicit() {
      let (_, na) = a.offset();
      let (_, nb) = b.offset();
      return if na >= nb { a } else { b };
    }
    // Structural equality.
    if a == b {
      return a;
    }
    // Zero absorption.
    if a.is_zero() {
      return b;
    }
    if b.is_zero() {
      return a;
    }
    // max(a, max(a, b')) = max(a, b'), max(a, max(b', a)) = max(b', a)
    if let UnivData::Max(bl, br, _) = b.data()
      && (*bl == a || *br == a)
    {
      return b;