Function and_env

crates/kernel/src/tutorial/defeq.rs:1241–1376

Build And : Prop → Prop → Prop with And.intro constructor.

()

    // the redundant post-rejection major WHNF enters this beta chain.
    let mut slow_proof = cnst("impossibleEq", &[]);
    for _ in 0..1024 {
      slow_proof = app(nlam("h", tf_eq.clone(), var(0)), slow_proof);
    }
    let (slow_id, slow) = mk_defn(
      "slowImpossibleEq",
      0,
      vec![],
      tf_eq,
      slow_proof,
      ix_common::env::ReducibilityHints::Abbrev,
    );
    env.insert(slow_id, slow);

    let motive = nlam(
      "_",
      cnst("Bool", &[]),
      nlam(
        "_",
        apps(
          cnst("Eq", &[usucc(uzero())]),
          &[cnst("Bool", &[]), cnst("Bool.true", &[]), var(0)],
        ),
        cnst("Bool", &[]),
      ),
    );
    let rec_app = apps(
      cnst("Eq.rec", &[usucc(uzero()), usucc(uzero())]),
      &[
        cnst("Bool", &[]),
        cnst("Bool.true", &[]),
        motive,
        cnst("Bool.true", &[]),
        cnst("Bool.false", &[]),
        cnst("slowImpossibleEq", &[]),
      ],
    );

    let mut tc = crate::tc::TypeChecker::new(&mut env);
    tc.rec_fuel = 512;
    let reduced = tc.whnf(&rec_app).expect(
      "a definitive K rejection should not normalize the expensive major",
    );
    assert_eq!(reduced.hash_key(), rec_app.hash_key());
  }

  // ==========================================================================
  // Projection tests (Tutorial.lean 760–900)
  // Requires And as structure
  // ==========================================================================

  /// Build And : Prop → Prop → Prop with And.intro constructor.
  fn and_env() -> KEnv<Meta> {
    let mut env = KEnv::<Meta>::new();
    add_eq_axioms(&mut env);

    let n = "And";
    let block_id = mk_id(n);
    let intro_id = mk_id("And.intro");