()
| 758 | |
| 759 | // Acc.rec.{1,1} (fun _ _ _ => p) h : should NOT reduce |
| 760 | let motive = nlam( |
| 761 | "x", |
| 762 | var(4), |
| 763 | nlam( |
| 764 | "_", |
| 765 | apps(cnst("Acc", &[usucc(uzero())]), &[var(5), var(4), var(0)]), |
| 766 | cnst("Bool", &[]), |
| 767 | ), |
| 768 | ); |
| 769 | let rec_app = apps( |
| 770 | cnst("Acc.rec", &[usucc(uzero()), usucc(uzero())]), |
| 771 | &[ |
| 772 | var(4), // α |
| 773 | var(3), // r |
| 774 | motive, // motive |
| 775 | var(2), // x = a |
| 776 | var(1), // t = h |
| 777 | ], |
| 778 | ); |
| 779 | |
| 780 | let ty = ipi( |
| 781 | "α", |
| 782 | sort1(), |
| 783 | npi( |
| 784 | "r", |
| 785 | pi(var(0), pi(var(1), sort0())), |
| 786 | npi( |
| 787 | "a", |
| 788 | var(1), |
| 789 | npi( |
| 790 | "h", |
| 791 | acc_r_a.clone(), |
| 792 | npi( |
| 793 | "p", |
| 794 | cnst("Bool", &[]), |
| 795 | eq_expr(usucc(uzero()), cnst("Bool", &[]), rec_app, var(0)), |
| 796 | ), |
| 797 | ), |
| 798 | ), |
| 799 | ), |
| 800 | ); |
| 801 | |
| 802 | // Value: fun α r a h p => Eq.refl p (BOGUS — claims reduction happened) |
| 803 | let val = ME::lam( |
| 804 | mk_name("α"), |
| 805 | ix_common::env::BinderInfo::Implicit, |
| 806 | sort1(), |
| 807 | nlam( |
| 808 | "r", |
| 809 | pi(var(0), pi(var(1), sort0())), |
| 810 | nlam( |
| 811 | "a", |
| 812 | var(1), |
| 813 | nlam( |
| 814 | "h", |
| 815 | apps(cnst("Acc", &[usucc(uzero())]), &[var(2), var(1), var(0)]), |
| 816 | nlam( |
| 817 | "p", |
nothing calls this directly
no test coverage detected