Add Eq as a full inductive (not just axioms) — needed for Quot.lift validation.
(env: &mut KEnv<Meta>)
| 1365 | params: 2, |
| 1366 | indices: 1, |
| 1367 | is_unsafe: false, |
| 1368 | block: eq_id.clone(), |
| 1369 | member_idx: 0, |
| 1370 | ty: eq_ty, |
| 1371 | ctors: vec![refl_id.clone()], |
| 1372 | lean_all: vec![eq_id.clone()], |
| 1373 | }, |
| 1374 | ); |
| 1375 | |
| 1376 | let eq_refl_ty = ipi( |
| 1377 | "α", |
| 1378 | sort(param(0)), |
| 1379 | npi( |
| 1380 | "a", |
| 1381 | var(0), |
| 1382 | apps(cnst("Eq", &[param(0)]), &[var(1), var(0), var(0)]), |
| 1383 | ), |
| 1384 | ); |
| 1385 | env.insert( |
| 1386 | refl_id.clone(), |
| 1387 | KConst::Ctor { |
| 1388 | name: mk_name("Eq.refl"), |
| 1389 | level_params: vec![mk_name("u")], |
| 1390 | is_unsafe: false, |
| 1391 | lvls: 1, |
| 1392 | induct: eq_id.clone(), |
| 1393 | cidx: 0, |
| 1394 | params: 2, |
| 1395 | fields: 0, |
| 1396 | ty: eq_refl_ty, |
| 1397 | }, |
| 1398 | ); |
| 1399 | |
| 1400 | // Minimal Eq.rec (k=true) |
| 1401 | let eq_a_aprime = apps(cnst("Eq", &[param(1)]), &[var(2), var(1), var(0)]); |
| 1402 | let motive_ty = npi("a'", var(1), pi(eq_a_aprime, sort(param(0)))); |
| 1403 | let eq_refl_a = apps(cnst("Eq.refl", &[param(1)]), &[var(2), var(1)]); |
| 1404 | let minor_refl = app(app(var(0), var(1)), eq_refl_a); |
| 1405 | let eq_a_aprime_d5 = |
| 1406 | apps(cnst("Eq", &[param(1)]), &[var(4), var(3), var(0)]); |
| 1407 | let result = app(app(var(3), var(1)), var(0)); |
| 1408 | let eq_rec_ty = ipi( |
| 1409 | "α", |
| 1410 | sort(param(1)), |
| 1411 | ipi( |
| 1412 | "a", |
| 1413 | var(0), |
| 1414 | ipi( |
| 1415 | "motive", |
| 1416 | motive_ty, |
| 1417 | npi( |
| 1418 | "refl", |
| 1419 | minor_refl, |
| 1420 | ipi("a'", var(3), npi("t", eq_a_aprime_d5, result)), |
| 1421 | ), |
| 1422 | ), |
| 1423 | ), |
| 1424 | ); |
no test coverage detected