Build a simple structure T with val : Bool, proof : True
()
| 2087 | &[ |
| 2088 | bool_ty.clone(), // α = Bool |
| 2089 | cnst("Bool.true", &[]), // a = true |
| 2090 | motive, // motive: fun _ _ => Bool |
| 2091 | a_applied, // refl minor = a (Eq.refl true) : Bool |
| 2092 | ], |
| 2093 | ); |
| 2094 | // rec_partial has 4 args but Eq.rec needs 6. So rec_partial : {a' : Bool} → (true = a') → Bool |
| 2095 | |
| 2096 | // The key claim (bogus): rec_partial = a |
| 2097 | // Both have type (true = true → Bool), but they're not def-eq because |
| 2098 | // partial recursor application should not trigger eta expansion. |
| 2099 | let lhs = rec_partial; |
| 2100 | let ty = |
| 2101 | npi("a", a_ty.clone(), eq_expr(u1.clone(), a_ty.clone(), lhs, var(0))); |
| 2102 | let val = nlam("a", a_ty, eq_refl_expr(u1, pi(tt_eq, bool_ty), var(0))); |
| 2103 | |
| 2104 | let (id, c) = mk_defn( |
| 2105 | "etaRuleK", |
| 2106 | 0, |
| 2107 | vec![], |
| 2108 | ty, |
| 2109 | val, |
| 2110 | ix_common::env::ReducibilityHints::Opaque, |
| 2111 | ); |
| 2112 | env.insert(id.clone(), c); |
| 2113 | check_rejects(&mut env, &id); |
| 2114 | } |
| 2115 | |
| 2116 | // ========================================================================== |
| 2117 | // etaCtor corner case (Tutorial.lean 1001–1013) |
| 2118 | // |
| 2119 | // Partially applied constructor should NOT trigger eta expansion. |
| 2120 | // T.mk (x True.intro).val ≠ x even though T.mk applied to both |
| 2121 | // fields would reconstruct the structure. |
| 2122 | // ========================================================================== |
| 2123 | |
| 2124 | /// Build a simple structure T with val : Bool, proof : True |
| 2125 | fn t_struct_env() -> KEnv<Meta> { |
| 2126 | let mut env = eq_inductive_env(); |
| 2127 | |
| 2128 | // True : Prop, single ctor True.intro |
| 2129 | let true_ty_id = mk_id("True"); |
| 2130 | let true_intro_id = mk_id("True.intro"); |
| 2131 | let true_rec_id = mk_id("True.rec"); |
| 2132 | |
| 2133 | env.insert( |
| 2134 | true_ty_id.clone(), |
| 2135 | KConst::Indc { |
| 2136 | name: mk_name("True"), |
| 2137 | level_params: vec![], |
| 2138 | lvls: 0, |
| 2139 | params: 0, |
| 2140 | indices: 0, |
| 2141 | is_unsafe: false, |
| 2142 | block: true_ty_id.clone(), |
| 2143 | member_idx: 0, |
| 2144 | ty: sort0(), |
| 2145 | ctors: vec![true_intro_id.clone()], |
| 2146 | lean_all: vec![true_ty_id.clone()], |