Method try_normalize_int_decidable

crates/kernel/src/whnf.rs:2360–2399

(
    &mut self,
    addr: &Address,
    args: &[KExpr<M>],
  )

  fn try_reduce_nat_with_succ_mode(
    &mut self,
    e: &KExpr<M>,
    nat_succ_mode: NatSuccMode,
  ) -> Result<Option<KExpr<M>>, TcError<M>> {
    let (head, args) = collect_app_spine(e);
    let addr = match head.data() {
      ExprData::Const(id, _, _) => id.addr.clone(),
      _ => return Ok(None),
    };
    // Nat.succ n → n + 1
    if addr == self.prims.nat_succ.addr && args.len() == 1 {
      if nat_succ_mode == NatSuccMode::Stuck {
        return Ok(None);
      }
      return self.try_reduce_nat_succ_iter(&args[0]);
    }

    if args.len() < 2 {
      return Ok(None);
    }

    let is_bin_arith = self.is_nat_bin_arith_addr(&addr);
    let is_bin_pred = self.is_nat_bin_pred_addr(&addr);

    if !is_bin_arith && !is_bin_pred {
      return Ok(None);
    }
    self.dump_nat_trace("candidate", e);

    if is_bin_pred {
      return self.try_reduce_nat_predicate(&addr, &args);
    }

    let Some(wa) = self.whnf_prim_arg(&args[0])? else {
      return Ok(None);
    };
    let Some(wb) = self.whnf_prim_arg(&args[1])? else {
      return Ok(None);
    };
    self.dump_nat_trace("arg0-whnf", &wa);
    self.dump_nat_trace("arg1-whnf", &wb);
    let a_val = match extract_nat_lit(&wa, &self.prims) {
      Some(v) => v.clone(),
      None => {