()
| 6599 | member_idx: 0, |
| 6600 | ty: list_ty, |
| 6601 | ctors: vec![mk_id("List.nil"), mk_id("List.cons")], |
| 6602 | lean_all: (), |
| 6603 | }, |
| 6604 | ); |
| 6605 | let nil_ty = pi(AE::sort(param(0)), app(cnst("List", &[param(0)]), var(0))); |
| 6606 | env.insert( |
| 6607 | mk_id("List.nil"), |
| 6608 | KConst::Ctor { |
| 6609 | name: (), |
| 6610 | level_params: (), |
| 6611 | is_unsafe: false, |
| 6612 | lvls: 1, |
| 6613 | induct: mk_id("List"), |
| 6614 | cidx: 0, |
| 6615 | params: 1, |
| 6616 | fields: 0, |
nothing calls this directly
no test coverage detected