Method try_def_eq_offset

crates/kernel/src/def_eq.rs:971–991

M2: Nat offset reduction for lazy delta loop (lean4lean isDefEqOffset). Returns Some(true/false) if both are nat-zero or nat-succ, None otherwise.

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

          return id.addr == p.nat_zero.addr
            || id.addr == p.nat_succ.addr
            || id.addr == p.nat_add.addr;
        },
        ExprData::App(f, _, _) => cur = f,
        _ => return false,
      }
    }
  }

  /// If expression is nat-succ, return the predecessor.
  /// Matches both `Nat(n+1)` → `Nat(n)` and `Nat.succ e` → `e`.
  fn nat_succ_of(&mut self, e: &KExpr<M>) -> Option<KExpr<M>> {
    match e.data() {
      ExprData::Nat(v, _, _) => {
        if v.0 == num_bigint::BigUint::ZERO {
          return None;
        }
        let pred = bignat::Nat(&v.0 - num_bigint::BigUint::from(1u64));
        let pred_addr = ix_common::address::Address::hash(&pred.to_le_bytes());
        Some(self.env.intern.intern_expr(KExpr::nat(pred, pred_addr)))
      },
      ExprData::App(f, arg, _) => match f.data() {
        ExprData::Const(id, _, _) if id.addr == self.prims.nat_succ.addr => {
          Some(arg.clone())
        },