| 1275 | name: (), |
| 1276 | level_params: (), |
| 1277 | is_unsafe: false, |
| 1278 | lvls: 1, |
| 1279 | induct: prims.eq.clone(), |
| 1280 | cidx: 0, |
| 1281 | params: 2, |
| 1282 | fields: 0, |
| 1283 | ty, |
| 1284 | }, |
| 1285 | ); |
| 1286 | } |
| 1287 | |
| 1288 | /// A well-typed type with the old minimum number of leading foralls but no |
| 1289 | /// quotient semantics. Every variant below was accepted by the former |
| 1290 | /// arity-only gate when installed directly at a reserved primitive KId. |
| 1291 | fn forged_forall_type(n: usize) -> AE { |
| 1292 | (0..n).fold(sort0(), |body, _| AE::all((), (), sort0(), body)) |
| 1293 | } |
| 1294 | |
| 1295 | fn forged_eq_type() -> AE { |
| 1296 | let u = AU::param(0, ()); |