()
| 347 | |
| 348 | // I : Prop → Type (1 param) |
| 349 | env.insert( |
| 350 | block_id.clone(), |
| 351 | KConst::Indc { |
| 352 | name: mk_name(n), |
| 353 | level_params: vec![], |
| 354 | lvls: 0, |
| 355 | params: 1, |
| 356 | indices: 0, |
| 357 | is_unsafe: false, |
| 358 | block: block_id.clone(), |
| 359 | member_idx: 0, |
| 360 | ty: pi(sort0(), sort1()), |
| 361 | ctors: vec![ctor_id.clone()], |
| 362 | lean_all: vec![block_id.clone()], |
| 363 | }, |
| 364 | ); |
| 365 | |
| 366 | // mk : ∀ (x : Type), I aProp — passes aProp instead of x as param |
| 367 | // At depth 1 (inside x binder): x = var(0) |
| 368 | env.insert( |
| 369 | ctor_id.clone(), |
| 370 | KConst::Ctor { |
| 371 | name: mk_name(&format!("{n}.mk")), |
| 372 | level_params: vec![], |
| 373 | is_unsafe: false, |
| 374 | lvls: 0, |
| 375 | induct: block_id.clone(), |
| 376 | cidx: 0, |
| 377 | params: 1, |
| 378 | fields: 0, |
| 379 | ty: npi("x", sort1(), app(cnst(n, &[]), cnst("aProp", &[]))), |
| 380 | }, |
| 381 | ); |
| 382 | |
| 383 | // Dummy recursor |
| 384 | let rec_ty = ipi( |
| 385 | "motive", |
| 386 | pi(sort0(), pi(app(cnst(n, &[]), var(0)), sort(param(0)))), |
| 387 | npi( |
| 388 | "t", |
| 389 | sort0(), |
| 390 | npi("x", app(cnst(n, &[]), var(0)), app(app(var(2), var(1)), var(0))), |
| 391 | ), |
| 392 | ); |
| 393 | env.insert( |
| 394 | rec_id.clone(), |
| 395 | KConst::Recr { |
| 396 | name: mk_name(&format!("{n}.rec")), |
| 397 | level_params: vec![mk_name("u")], |
| 398 | k: false, |
| 399 | is_unsafe: false, |
| 400 | lvls: 1, |
| 401 | params: 1, |
| 402 | indices: 0, |
| 403 | motives: 1, |
| 404 | minors: 0, |
| 405 | block: block_id.clone(), |
| 406 | member_idx: 0, |
nothing calls this directly
no test coverage detected