Method bitvec_to_nat_expr

crates/kernel/src/whnf.rs:2560–2573

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

    let mut total = base_val.0;
    total += parts.major.0;
    total += offset;
    let result = Nat(total);
    let blob_addr = Address::hash(&result.to_le_bytes());
    Ok(Some(KExpr::nat(result, blob_addr)))
  }

  fn nat_rec_literal_parts(
    &mut self,
    e: &KExpr<M>,
  ) -> Result<Option<NatRecLiteralParts<M>>, TcError<M>> {
    let (head, spine) = collect_app_spine(e);
    let ExprData::Const(id, _, _) = head.data() else {
      return Ok(None);
    };
    if id.addr != self.prims.nat_rec.addr {
      return Ok(None);
    }