Method try_reduce_bitvec_to_nat

crates/kernel/src/whnf.rs:2575–2608

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

    };
    if id.addr != self.prims.nat_rec.addr {
      return Ok(None);
    }

    let Some(KConst::Recr { params, motives, minors, indices, .. }) =
      self.try_get_const(id)?
    else {
      return Ok(None);
    };
    let params = u64_to_usize::<M>(params)?;
    let motives = u64_to_usize::<M>(motives)?;
    let minors = u64_to_usize::<M>(minors)?;
    let indices = u64_to_usize::<M>(indices)?;
    if minors < 2 {
      return Ok(None);
    }

    let base_idx = params + motives;
    let step_idx = base_idx + 1;
    let major_idx = params + motives + minors + indices;
    let Some(major) = spine.get(major_idx) else {
      return Ok(None);
    };
    let ExprData::Nat(major, _, _) = major.data() else {
      return Ok(None);
    };
    let major = major.clone();

    Ok(Some(NatRecLiteralParts { spine, major, base_idx, step_idx, major_idx }))
  }

  fn is_nat_succ_ih_step(
    &mut self,
    step: &KExpr<M>,
  ) -> Result<bool, TcError<M>> {
    let step = self.whnf(step)?;
    let ExprData::Lam(_, _, _, body, _) = step.data() else {
      return Ok(false);