()
| 1108 | let motive = nlam( |
| 1109 | "_", |
| 1110 | cnst("Bool", &[]), |
| 1111 | nlam( |
| 1112 | "_", |
| 1113 | apps( |
| 1114 | cnst("Eq", &[usucc(uzero())]), |
| 1115 | &[cnst("Bool", &[]), cnst("Bool.true", &[]), var(0)], |
| 1116 | ), |
| 1117 | cnst("Bool", &[]), |
| 1118 | ), |
| 1119 | ); |
| 1120 | let rec_app = apps( |
| 1121 | cnst("Eq.rec", &[usucc(uzero()), usucc(uzero())]), |
| 1122 | &[ |
| 1123 | cnst("Bool", &[]), // α |
| 1124 | cnst("Bool.true", &[]), // a |
| 1125 | motive, // motive: fun _ _ => Bool |
| 1126 | var(0), // refl case value = a (var(0) at depth 2) |
| 1127 | cnst("Bool.true", &[]), // a' = true (index) |
| 1128 | var(1), // t = h |
| 1129 | ], |
| 1130 | ); |
| 1131 | |
| 1132 | // type: ∀ (h : true = true) (a : Bool), Eq.{1} Bool (rec...) a |
| 1133 | let ty = npi( |
| 1134 | "h", |
| 1135 | tt_eq.clone(), |
| 1136 | npi( |
| 1137 | "a", |
| 1138 | cnst("Bool", &[]), |
| 1139 | eq_expr(usucc(uzero()), cnst("Bool", &[]), rec_app, var(0)), |
| 1140 | ), |
| 1141 | ); |
| 1142 | |
| 1143 | // value: fun h a => Eq.refl.{1} Bool a |
| 1144 | let val = nlam( |
| 1145 | "h", |
| 1146 | tt_eq, |
| 1147 | nlam( |
| 1148 | "a", |
| 1149 | cnst("Bool", &[]), |
| 1150 | eq_refl_expr(usucc(uzero()), cnst("Bool", &[]), var(0)), |
| 1151 | ), |
| 1152 | ); |
| 1153 | |
| 1154 | let (id, c) = mk_thm("ruleK", 0, vec![], ty, val); |
| 1155 | env.insert(id.clone(), c); |
| 1156 | check_accepts(&mut env, &id); |
| 1157 | } |
| 1158 | |
| 1159 | /// ruleKbad: ∀ (h : true = false) (a : Bool), Eq.rec (motive := fun _ _ => Bool) a h = a |
| 1160 | /// Rule K should NOT fire because the constructor indices don't match (true ≠ false). |
| 1161 | #[test] |
| 1162 | fn bad_rule_k() { |
| 1163 | let mut env = eq_inductive_env(); |
| 1164 | |
| 1165 | // true = false = @Eq Bool true false |
| 1166 | let tf_eq = apps( |
| 1167 | cnst("Eq", &[usucc(uzero())]), |
nothing calls this directly
no test coverage detected