Function add_eq_axioms

crates/kernel/src/testing.rs:201–215

Add Eq.{u} and Eq.refl.{u} as axioms to the environment. Eq : {α : Sort u} → α → α → Prop Eq.refl : {α : Sort u} → (a : α) → Eq a a

(env: &mut KEnv<Meta>)

/// Eq : {α : Sort u} → α → α → Prop
/// Eq.refl : {α : Sort u} → (a : α) → Eq a a
pub fn add_eq_axioms(env: &mut KEnv<Meta>) {
  let eq_ty =
    ipi("α", sort(param(0)), npi("a", var(0), npi("b", var(1), sort0())));
  let (eq_id, eq_c) = mk_axiom("Eq", 1, vec![mk_name("u")], eq_ty);
  env.insert(eq_id, eq_c);

  let eq_refl_ty = ipi(
    "α",
    sort(param(0)),
    npi("a", var(0), apps(cnst("Eq", &[param(0)]), &[var(1), var(0), var(0)])),
  );
  let (refl_id, refl_c) =
    mk_axiom("Eq.refl", 1, vec![mk_name("u")], eq_refl_ty);
  env.insert(refl_id, refl_c);
}

/// Convenience: Eq.{u} α a b
pub fn eq_expr(u: MU, alpha: ME, a: ME, b: ME) -> ME {