Function good_nat_lit

crates/kernel/src/tutorial/reduction.rs:980–999

()

    // aNatLit : N := NatVal(0)
    use bignat::Nat;
    use ix_common::address::Address;
    let nat_0 = ME::nat(Nat::from(0u64), Address::hash(b"natval_0"));
    let (id, c) =
      mk_defn("aNatLit", 0, vec![], nat(), nat_0, ReducibilityHints::Opaque);
    env.insert(id.clone(), c);
    let mut prims = test_prims(&env);
    prims.nat = mk_id("N");
    prims.nat_zero = mk_id("N.zero");
    prims.nat_succ = mk_id("N.succ");
    check_accepts_with_prims(&mut env, &id, prims);
  }

  /// natLitEq : Eq N 3 (N.succ (N.succ (N.succ N.zero))) := Eq.refl 3
  /// Nat literal 3 must reduce to succ(succ(succ(zero))).
  #[test]
  fn good_nat_lit_eq() {
    let mut env = nat_env();
    let nat = || cnst("N", &[]);

    use bignat::Nat;
    use ix_common::address::Address;

    let nat_3 = ME::nat(Nat::from(3u64), Address::hash(b"natval_3"));