Function compute_nat_bin

crates/kernel/src/whnf.rs:2905–2970

Compute a binary nat operation. Returns `None` if the operation can't be computed (e.g., exponent too large) — caller leaves the expression unreduced.

(
  addr: &Address,
  p: &Primitives<M>,
  a: &Nat,
  b: &Nat,
)

      Some(v) => v,
      None => return Ok(None),
    };
    let b_val = match extract_nat_value(&wb, &self.prims) {
      Some(v) => v,
      None => return Ok(None),
    };

    // S5: Eq.refl is universe-polymorphic: @Eq.refl.{u}.
    // For Bool : Type = Sort 1, we need u = 1 = Succ(Zero).
    let u1 = KUniv::succ(KUniv::zero());

    // decLt n m  →  decLe (n+1) m
    if is_dec_lt {
      let succ_a = Nat(&a_val.0 + 1u64);
      let succ_a_addr = Address::hash(&succ_a.to_le_bytes());
      let succ_a_expr = self.intern(KExpr::nat(succ_a, succ_a_addr));
      // Build: Nat.decLe (n+1) m
      let dec_le_const =
        self.intern(KExpr::cnst(self.prims.nat_dec_le.clone(), Box::new([])));
      let mut result = self.intern(KExpr::app(dec_le_const, succ_a_expr));
      result = self.intern(KExpr::app(result, args[1].clone()));
      for arg in args.iter().skip(2) {
        result = self.intern(KExpr::app(result, arg.clone()));
      }
      // Recursively reduce the decLe
      return Ok(Some(result));
    }

    // Extract the proposition from the type of `e`.
    // `e : Decidable prop` → we need `prop` as the first constructor argument.
    // Use infer_only to avoid def-eq checks (safe within WHNF).
    let prop = match self.with_infer_only(|tc| tc.infer(e)) {
      Ok(e_ty) => {
        let e_ty_whnf = self.whnf(&e_ty)?;
        let (_, type_args) = collect_app_spine(&e_ty_whnf);
        match type_args.into_iter().next() {
          Some(p) => p,
          None => return Ok(None), // not `Decidable prop` — bail
        }
      },
      Err(_) => return Ok(None), // inference failed — bail to delta
    };

    let (b_result, proof_true_fn, proof_false_fn) = if is_dec_le {
      (
        a_val <= b_val,
        &self.prims.nat_le_of_ble_eq_true,
        &self.prims.nat_not_le_of_not_ble_eq_true,
      )
    } else {
      // is_dec_eq
      (
        a_val == b_val,
        &self.prims.nat_eq_of_beq_eq_true,
        &self.prims.nat_ne_of_beq_eq_false,
      )
    };
    let proof_true_fn = proof_true_fn.clone();
    let proof_false_fn = proof_false_fn.clone();