Function good_peano1

crates/kernel/src/tutorial/reduction.rs:174–198

()

  /// peano1 : ∀ (t : PN → Prop) (v : (n : PN) → t n), t PN.lit2 := fun t v => v PN.lit2
  #[test]
  fn good_peano1() {
    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", &[])),
      ),
    );
    let val = nlam(
      "t",
      pi(cnst("PN", &[]), sort0()),
      nlam(
        "v",
        npi("n", cnst("PN", &[]), app(var(1), var(0))),
        app(var(0), cnst("PN.lit2", &[])),
      ),
    );
    let mut env2 = env;
    let (id, c) = mk_thm("peano1", 0, vec![], ty, val);
    env2.insert(id.clone(), c);
    check_accepts(&mut env2, &id);
  }

  /// peano2 : ∀ (t : PN → Prop) (v : (n : PN) → t n), t PN.lit2 := fun t v => v (PN.add PN.lit1 PN.lit1)
  /// Tests that 1 + 1 reduces to 2 via Church numeral reduction.