()
| 435 | KConst::Indc { |
| 436 | name: mk_name(n), |
| 437 | level_params: vec![], |
| 438 | lvls: 0, |
| 439 | params: 0, |
| 440 | indices: 0, |
| 441 | is_unsafe: false, |
| 442 | block: block_id.clone(), |
| 443 | member_idx: 0, |
| 444 | ty: sort1(), |
| 445 | ctors: vec![ctor_id.clone()], |
| 446 | lean_all: vec![block_id.clone()], |
| 447 | }, |
| 448 | ); |
| 449 | |
| 450 | // mk : (Nat → (I → Nat)) → I |
| 451 | // The field type is Nat → (I → Nat), I occurs in negative position (left of inner arrow) |
| 452 | let field_ty = pi(cnst("Nat", &[]), pi(cnst(n, &[]), cnst("Nat", &[]))); |
| 453 | env.insert( |
| 454 | ctor_id.clone(), |
| 455 | KConst::Ctor { |
| 456 | name: mk_name(&format!("{n}.mk")), |
| 457 | level_params: vec![], |
| 458 | is_unsafe: false, |
| 459 | lvls: 0, |
| 460 | induct: block_id.clone(), |
| 461 | cidx: 0, |
| 462 | params: 0, |
| 463 | fields: 1, |
| 464 | ty: pi(field_ty, cnst(n, &[])), |
| 465 | }, |
| 466 | ); |
| 467 | |
| 468 | // Dummy recursor |
| 469 | let rec_ty = npi( |
| 470 | "motive", |
| 471 | pi(cnst(n, &[]), sort(param(0))), |
| 472 | npi( |
| 473 | "mk", |
| 474 | pi( |
| 475 | pi(cnst("Nat", &[]), pi(cnst(n, &[]), cnst("Nat", &[]))), |
| 476 | app(var(1), cnst(n, &[])), |
| 477 | ), |
| 478 | npi("t", cnst(n, &[]), app(var(2), var(0))), |
| 479 | ), |
| 480 | ); |
| 481 | env.insert( |
| 482 | rec_id.clone(), |
| 483 | KConst::Recr { |
| 484 | name: mk_name(&format!("{n}.rec")), |
| 485 | level_params: vec![mk_name("u")], |
| 486 | k: false, |
| 487 | is_unsafe: false, |
| 488 | lvls: 1, |
| 489 | params: 0, |
| 490 | indices: 0, |
| 491 | motives: 1, |
| 492 | minors: 1, |
| 493 | block: block_id.clone(), |
| 494 | member_idx: 0, |
nothing calls this directly
no test coverage detected