Method nat_succ_of

crates/kernel/src/def_eq.rs:926–944

If expression is nat-succ, return the predecessor. Matches both `Nat(n+1)` → `Nat(n)` and `Nat.succ e` → `e`.

(&mut self, e: &KExpr<M>)

      return Ok(false);
    }
    // Both must have the same type
    let b_ty = match self.with_infer_only(|tc| tc.infer(b)) {
      Ok(ty) => ty,
      Err(_) => return Ok(false),
    };
    self.is_def_eq(&a_ty_w, &b_ty)
  }

  // -----------------------------------------------------------------------
  // Nat literal ↔ constructor comparison
  // -----------------------------------------------------------------------

  /// Check if an expression is a nat-like value (literal, Nat.zero, Nat.succ _).
  fn is_nat_like(&self, e: &KExpr<M>) -> bool {
    match e.data() {
      ExprData::Nat(..) => true,
      ExprData::Const(id, _, _) => id.addr == self.prims.nat_zero.addr,
      ExprData::App(f, _, _) => {
        matches!(f.data(), ExprData::Const(id, _, _) if id.addr == self.prims.nat_succ.addr)
      },
      _ => false,
    }