Function usize_env

crates/kernel/src/whnf.rs:4213–4321

Build an env that includes the full USize.size reduction chain: System.Platform.numBits (handled by try_reduce_native → 64) Nat.pow at the correct primitive address USize.size := Nat.pow 2 numBits (reducible def)

()

    let lam = AE::lam((), (), sort0(), body);
    let app = AE::app(lam, opaque.clone());
    assert_eq!(tc.whnf(&app).unwrap(), opaque);
  }

  #[test]
  fn whnf_machine_closure_iota_via_beta() {
    use super::super::constant::RecRule;
    // A beta whose body is a recursor application: the machine's Const
    // exit must take the closure-iota path (rule args ride through as
    // closures) and produce the same result as the eager iota.
    //
    // Unit-like inductive `U` with one ctor `U.mk` (no params/fields)
    // and recursor `U.rec : (motive) (minor) (major) → minor`.
    let u_id = mk_id("Test.U");
    let u_mk_id = mk_id("Test.U.mk");
    let u_rec_id = mk_id("Test.U.rec");
    let mut env = env_with_id();
    env.insert(
      u_id.clone(),
      KConst::Indc {
        name: (),
        level_params: (),
        lvls: 0,
        params: 0,
        indices: 0,
        is_unsafe: false,
        block: u_id.clone(),
        member_idx: 0,
        ty: sort0(),
        ctors: vec![u_mk_id.clone()],
        lean_all: (),
      },
    );
    env.insert(
      u_mk_id.clone(),
      KConst::Ctor {
        name: (),
        level_params: (),
        is_unsafe: false,
        lvls: 0,
        induct: u_id.clone(),
        cidx: 0,
        params: 0,
        fields: 0,
        ty: AE::cnst(u_id.clone(), Box::new([])),
      },
    );
    env.insert(
      u_rec_id.clone(),
      KConst::Recr {
        name: (),
        level_params: (),
        k: false,
        is_unsafe: false,
        lvls: 0,
        params: 0,
        indices: 0,
        motives: 1,
        minors: 1,