()
| 526 | lvls: 0, |
| 527 | params: 0, |
| 528 | indices: 1, |
| 529 | is_unsafe: false, |
| 530 | block: block_id.clone(), |
| 531 | member_idx: 0, |
| 532 | ty: npi("α", sort1(), sort1()), |
| 533 | ctors: vec![ctor_id.clone()], |
| 534 | lean_all: vec![block_id.clone()], |
| 535 | }, |
| 536 | ); |
| 537 | |
| 538 | // mk : (α : Type) → (Nat → I (I α)) → I α |
| 539 | // At depth 1 (inside α): α = var(0) |
| 540 | // field: Nat → I (I α) — I applied to (I α), recursive in index |
| 541 | let i_alpha = app(cnst(n, &[]), var(0)); // I α |
| 542 | let i_i_alpha = app(cnst(n, &[]), i_alpha); // I (I α) |
| 543 | let _field_ty = pi(cnst("Nat", &[]), i_i_alpha); // Nat → I (I α), shifts inside pi |
| 544 | // But inside the field pi: Nat binder is var(0), α = var(1) |
| 545 | // So we need: pi(Nat, I(I(var(1)))) — var(1) = α shifted |
| 546 | let i_alpha_s = app(cnst(n, &[]), var(1)); |
| 547 | let i_i_alpha_s = app(cnst(n, &[]), i_alpha_s); |
| 548 | let field_ty_correct = pi(cnst("Nat", &[]), i_i_alpha_s); |
| 549 | let result = app(cnst(n, &[]), var(1)); // I α, with α shifted by field binder |
| 550 | env.insert( |
| 551 | ctor_id.clone(), |
| 552 | KConst::Ctor { |
| 553 | name: mk_name(&format!("{n}.mk")), |
| 554 | level_params: vec![], |
| 555 | is_unsafe: false, |
| 556 | lvls: 0, |
| 557 | induct: block_id.clone(), |
| 558 | cidx: 0, |
| 559 | params: 0, |
| 560 | fields: 1, |
| 561 | ty: npi("α", sort1(), pi(field_ty_correct, result)), |
| 562 | }, |
| 563 | ); |
| 564 | |
| 565 | // Dummy recursor |
| 566 | let rec_ty = npi( |
| 567 | "motive", |
| 568 | pi(sort1(), pi(app(cnst(n, &[]), var(0)), sort(param(0)))), |
| 569 | npi( |
| 570 | "t", |
| 571 | sort1(), |
| 572 | npi("x", app(cnst(n, &[]), var(0)), app(app(var(2), var(1)), var(0))), |
| 573 | ), |
| 574 | ); |
| 575 | env.insert( |
| 576 | rec_id.clone(), |
| 577 | KConst::Recr { |
| 578 | name: mk_name(&format!("{n}.rec")), |
| 579 | level_params: vec![mk_name("u")], |
| 580 | k: false, |
| 581 | is_unsafe: false, |
| 582 | lvls: 1, |
| 583 | params: 0, |
| 584 | indices: 1, |
| 585 | motives: 1, |
nothing calls this directly
no test coverage detected