Build environment with Bool + Eq as full inductives (not just axioms). Eq.{u} : {α : Sort u} → α → α → Prop (indexed, 2 params, 1 index) Eq.refl.{u} : {α : Sort u} → (a : α) → Eq a a Eq.rec.{u,v} with k = true (enables Rule K)
()
| 847 | let bool_rec_id = mk_id("Bool.rec"); |
| 848 | |
| 849 | env.insert( |
| 850 | bool_id.clone(), |
| 851 | KConst::Indc { |
| 852 | name: mk_name("Bool"), |
| 853 | level_params: vec![], |
| 854 | lvls: 0, |
| 855 | params: 0, |
| 856 | indices: 0, |
| 857 | is_unsafe: false, |
| 858 | block: bool_id.clone(), |
| 859 | member_idx: 0, |
| 860 | ty: sort1(), |
| 861 | ctors: vec![false_id.clone(), true_id.clone()], |
| 862 | lean_all: vec![bool_id.clone()], |
| 863 | }, |
| 864 | ); |
| 865 | env.insert( |
| 866 | false_id.clone(), |
| 867 | KConst::Ctor { |
| 868 | name: mk_name("Bool.false"), |
| 869 | level_params: vec![], |
| 870 | is_unsafe: false, |
| 871 | lvls: 0, |
| 872 | induct: bool_id.clone(), |
| 873 | cidx: 0, |
| 874 | params: 0, |
| 875 | fields: 0, |
| 876 | ty: cnst("Bool", &[]), |
| 877 | }, |
| 878 | ); |
| 879 | env.insert( |
| 880 | true_id.clone(), |
| 881 | KConst::Ctor { |
| 882 | name: mk_name("Bool.true"), |
| 883 | level_params: vec![], |
| 884 | is_unsafe: false, |
| 885 | lvls: 0, |
| 886 | induct: bool_id.clone(), |
| 887 | cidx: 1, |
| 888 | params: 0, |
| 889 | fields: 0, |
| 890 | ty: cnst("Bool", &[]), |
| 891 | }, |
| 892 | ); |
| 893 | // Bool.rec (minimal, no rules needed for these tests) |
| 894 | let bm = pi(cnst("Bool", &[]), sort(param(0))); |
| 895 | let bm_f = app(var(0), cnst("Bool.false", &[])); |
| 896 | let bm_t = app(var(1), cnst("Bool.true", &[])); |
| 897 | let bool_rec_ty = ipi( |
| 898 | "motive", |
| 899 | bm, |
| 900 | npi( |
| 901 | "hf", |
| 902 | bm_f, |
| 903 | npi("ht", bm_t, npi("t", cnst("Bool", &[]), app(var(3), var(0)))), |
| 904 | ), |
| 905 | ); |
| 906 | env.insert( |