Function good_peano2

crates/kernel/src/tutorial/reduction.rs:203–230

()

  /// Tests that 1 + 1 reduces to 2 via Church numeral reduction.
  #[test]
  fn good_peano2() {
    let env = peano_env();
    let ty = npi(
      "t",
      pi(cnst("PN", &[]), sort0()),
      npi(
        "v",
        npi("n", cnst("PN", &[]), app(var(1), var(0))),
        app(var(1), cnst("PN.lit2", &[])),
      ),
    );
    // Value uses add lit1 lit1 instead of lit2
    let one_plus_one =
      app(app(cnst("PN.add", &[]), cnst("PN.lit1", &[])), cnst("PN.lit1", &[]));
    let val = nlam(
      "t",
      pi(cnst("PN", &[]), sort0()),
      nlam(
        "v",
        npi("n", cnst("PN", &[]), app(var(1), var(0))),
        app(var(0), one_plus_one),
      ),
    );
    let mut env2 = env;
    let (id, c) = mk_thm("peano2", 0, vec![], ty, val);
    env2.insert(id.clone(), c);
    check_accepts(&mut env2, &id);
  }

  /// peano3 : ∀ (t : PN → Prop) (v : (n : PN) → t n), t PN.lit4 := fun t v => v (PN.mul PN.lit2 PN.lit2)
  /// Tests that 2 * 2 reduces to 4 via Church numeral reduction.