Function extract_nat_value

crates/kernel/src/whnf.rs:2870–2887

Extract a Nat value from either literal form or a constructor numeral. Iota reduction on `Nat` literals can expose the matched value as `Nat.succ ` inside branch bodies. Some non-Nat primitive helpers recover that value here before deciding whether a surrounding native reduction can proceed.

(
  e: &KExpr<M>,
  prims: &Primitives<M>,
)

  /// - decLe true:  `Decidable.isTrue  prop (Nat.le_of_ble_eq_true  n m (Eq.refl.{1} Bool Bool.true))`
  /// - decEq true:  `Decidable.isTrue  prop (Nat.eq_of_beq_eq_true  n m (Eq.refl.{1} Bool Bool.true))`
  /// - decEq false: `Decidable.isFalse prop (Nat.ne_of_beq_eq_false n m (Eq.refl.{1} Bool Bool.false))`
  /// - decLe false: falls through to delta (proof requires `False` primitive not yet available)
  /// - decLt n m:   delegates to decLe (n+1) m
  pub(super) fn try_reduce_decidable(
    &mut self,
    e: &KExpr<M>,
  ) -> 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),
    };

    let p = &self.prims;
    let is_dec_le = addr == p.nat_dec_le.addr;
    let is_dec_eq = addr == p.nat_dec_eq.addr;
    let is_dec_lt = addr == p.nat_dec_lt.addr;
    let is_int_dec_le = addr == p.int_dec_le.addr;
    let is_int_dec_eq = addr == p.int_dec_eq.addr;
    let is_int_dec_lt = addr == p.int_dec_lt.addr;
    if is_int_dec_le || is_int_dec_eq || is_int_dec_lt {