Method is_def_eq_nat

crates/kernel/src/def_eq.rs:949–967

Def-eq for nat-like values: handles mixed literal/constructor comparison. Fast-path: two Nat literals are compared directly by value (O(1) instead of O(n) recursion depth that would blow the def_eq_depth limit).

(
    &mut self,
    a: &KExpr<M>,
    b: &KExpr<M>,
  )

    }
  }

  /// Check if expression is nat zero (literal 0 or Nat.zero constructor).
  fn is_nat_zero(&self, e: &KExpr<M>) -> bool {
    match e.data() {
      ExprData::Nat(v, _, _) => v.0 == num_bigint::BigUint::ZERO,
      ExprData::Const(id, _, _) => id.addr == self.prims.nat_zero.addr,
      _ => false,
    }
  }

  /// Allocation-free check that `e` could decompose to `base + offset`:
  /// a Nat literal, `Nat.zero`/`Nat.succ`, or an app whose head constant is
  /// `Nat.succ`/`Nat.add`. Walks the app chain by reference — no spine Vec.
  fn nat_offset_candidate(&self, e: &KExpr<M>) -> bool {
    let mut cur = e;
    loop {
      match cur.data() {
        ExprData::Nat(..) => return true,
        ExprData::Const(id, _, _) => {
          let p = &self.prims;
          return id.addr == p.nat_zero.addr
            || id.addr == p.nat_succ.addr