()
| 257 | // typeWithTooHighTypeField : Sort 1 = Type |
| 258 | env.insert( |
| 259 | block_id.clone(), |
| 260 | KConst::Indc { |
| 261 | name: mk_name(n), |
| 262 | level_params: vec![], |
| 263 | lvls: 0, |
| 264 | params: 0, |
| 265 | indices: 0, |
| 266 | is_unsafe: false, |
| 267 | block: block_id.clone(), |
| 268 | member_idx: 0, |
| 269 | ty: sort1(), // Type = Sort 1 |
| 270 | ctors: vec![ctor_id.clone()], |
| 271 | lean_all: vec![block_id.clone()], |
| 272 | }, |
| 273 | ); |
| 274 | |
| 275 | // .mk : Sort 1 → typeWithTooHighTypeField |
| 276 | // Field of type Sort 1 = Type, but inductive is in Sort 1 = Type. |
| 277 | // Fields must be < Sort level of inductive, so Type (Sort 1) is too high for Type inductive. |
| 278 | env.insert( |
| 279 | ctor_id.clone(), |
| 280 | KConst::Ctor { |
| 281 | name: mk_name(&format!("{n}.mk")), |
| 282 | level_params: vec![], |
| 283 | is_unsafe: false, |
| 284 | lvls: 0, |
| 285 | induct: block_id.clone(), |
| 286 | cidx: 0, |
| 287 | params: 0, |
| 288 | fields: 1, |
| 289 | ty: pi(sort1(), cnst(n, &[])), // Sort 1 → I |
| 290 | }, |
| 291 | ); |
| 292 | |
| 293 | // Dummy recursor |
| 294 | let motive_ty = pi(cnst(n, &[]), sort(param(0))); |
| 295 | let minor = npi( |
| 296 | "α", |
| 297 | sort1(), |
| 298 | app(var(1), app(cnst(&format!("{n}.mk"), &[]), var(0))), |
| 299 | ); |
| 300 | let rec_ty = npi( |
| 301 | "motive", |
| 302 | motive_ty, |
| 303 | npi("mk", minor, npi("t", cnst(n, &[]), app(var(2), var(0)))), |
| 304 | ); |
| 305 | env.insert( |
| 306 | rec_id.clone(), |
| 307 | KConst::Recr { |
| 308 | name: mk_name(&format!("{n}.rec")), |
| 309 | level_params: vec![mk_name("u")], |
| 310 | k: false, |
| 311 | is_unsafe: false, |
| 312 | lvls: 1, |
| 313 | params: 0, |
| 314 | indices: 0, |
| 315 | motives: 1, |
| 316 | minors: 1, |
nothing calls this directly
no test coverage detected