Function good_trivial_eq

crates/kernel/src/tutorial/defeq.rs:227–246

()

  /// ∀ (p : Prop) (h : p), h = h
  #[test]
  fn good_trivial_eq() {
    let mut env = KEnv::<Meta>::new();
    add_eq_axioms(&mut env);

    // ∀ (p : Prop) (h : p), Eq.{0} p h h
    let ty = npi(
      "p",
      sort0(),
      npi("h", var(0), eq_expr(uzero(), var(1), var(0), var(0))),
    );
    // fun p h => Eq.refl.{0} p h
    let val = nlam(
      "p",
      sort0(),
      nlam("h", var(0), eq_refl_expr(uzero(), var(1), var(0))),
    );
    let (id, c) = mk_thm("trivialEq", 0, vec![], ty, val);
    env.insert(id.clone(), c);
    check_accepts(&mut env, &id);
  }

  /// bad: claim Eq.refl proves h1 = h2 for NON-Prop types (no proof irrelevance)
  /// ∀ (α : Type) (a b : α), Eq a b