()
| 1925 | |
| 1926 | /// Helper: build test `name : PropStructure.{0,1} → resType := fun x => .proj PropStructure idx x` |
| 1927 | fn mk_prop_structure_proj_test( |
| 1928 | env: &mut KEnv<Meta>, |
| 1929 | name: &str, |
| 1930 | res_ty: ME, |
| 1931 | idx: u64, |
| 1932 | ) -> MId { |
| 1933 | let ps01 = cnst("PropStructure", &[uzero(), usucc(uzero())]); |
| 1934 | let ty = pi(ps01.clone(), res_ty); |
| 1935 | let val = nlam("x", ps01, ME::prj(mk_id("PropStructure"), idx, var(0))); |
| 1936 | let (id, c) = mk_defn( |
| 1937 | name, |
| 1938 | 0, |
| 1939 | vec![], |
nothing calls this directly
no test coverage detected