Function good_peano3

crates/kernel/src/tutorial/reduction.rs:235–261

()

  /// Tests that 2 * 2 reduces to 4 via Church numeral reduction.
  #[test]
  fn good_peano3() {
    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.lit4", &[])),
      ),
    );
    let two_times_two =
      app(app(cnst("PN.mul", &[]), cnst("PN.lit2", &[])), cnst("PN.lit2", &[]));
    let val = nlam(
      "t",
      pi(cnst("PN", &[]), sort0()),
      nlam(
        "v",
        npi("n", cnst("PN", &[]), app(var(1), var(0))),
        app(var(0), two_times_two),
      ),
    );
    let mut env2 = env;
    let (id, c) = mk_thm("peano3", 0, vec![], ty, val);
    env2.insert(id.clone(), c);
    check_accepts(&mut env2, &id);
  }

  // ==========================================================================
  // Batch 13: Bool inductive + recursor reduction (Tutorial.lean 206, 693)