Build PUnit.{u} + Eq + PropStructure.{u,v} env.
()
| 1687 | env.insert( |
| 1688 | rec_id.clone(), |
| 1689 | KConst::Recr { |
| 1690 | name: mk_name(&format!("{n}.rec")), |
| 1691 | level_params: vec![mk_name("u"), mk_name("v")], |
| 1692 | k: false, |
| 1693 | is_unsafe: false, |
| 1694 | lvls: 2, |
| 1695 | params: 0, |
| 1696 | indices: 0, |
| 1697 | motives: 1, |
| 1698 | minors: 1, |
| 1699 | block: block_id.clone(), |
| 1700 | member_idx: 0, |
| 1701 | ty: rec_ty, |
| 1702 | rules: vec![], |
| 1703 | lean_all: vec![block_id.clone()], |
| 1704 | }, |
| 1705 | ); |
| 1706 | |
| 1707 | env |
| 1708 | .blocks |
| 1709 | .insert(block_id.clone(), vec![block_id.clone(), ctor_id, rec_id]); |
| 1710 | check_accepts(&mut env, &block_id); |
| 1711 | } |
| 1712 | |
| 1713 | // ========================================================================== |
| 1714 | // PropStructure projection tests (Tutorial.lean 791–848) |
| 1715 | // |
| 1716 | // PropStructure.{u,v} : Prop with 6 fields: |
| 1717 | // 0: aProof : PUnit.{u} — proof |
| 1718 | // 1: someData : PUnit.{v} — DATA |
| 1719 | // 2: aSecondProof : PUnit.{u} — proof |
| 1720 | // 3: someMoreData : PUnit.{v} — DATA |
| 1721 | // 4: aProofAboutData : someMoreData = someMoreData — proof (depends on data) |
| 1722 | // 5: aFinalProof : PUnit.{u} — proof (after dependent data) |
| 1723 | // |
| 1724 | // For Prop structures, projection restrictions apply: |
| 1725 | // - Data projections: FORBIDDEN |
| 1726 | // - Proof projections before dependent data: ALLOWED |
| 1727 | // - Any projection after dependent data field: FORBIDDEN |
| 1728 | // ========================================================================== |
| 1729 | |
| 1730 | /// Build PUnit.{u} + Eq + PropStructure.{u,v} env. |
| 1731 | fn prop_structure_env() -> KEnv<Meta> { |
| 1732 | let mut env = KEnv::<Meta>::new(); |
| 1733 | add_eq_axioms(&mut env); |
| 1734 | |
| 1735 | // -- PUnit.{u} : Sort u, PUnit.unit.{u} : PUnit.{u} -- |
| 1736 | let pu_id = mk_id("PUnit"); |
| 1737 | let pu_unit_id = mk_id("PUnit.unit"); |
| 1738 | let pu_rec_id = mk_id("PUnit.rec"); |
| 1739 | |
| 1740 | env.insert( |
| 1741 | pu_id.clone(), |
| 1742 | KConst::Indc { |
| 1743 | name: mk_name("PUnit"), |
| 1744 | level_params: vec![mk_name("u")], |
| 1745 | lvls: 1, |
| 1746 | params: 0, |