()
| 5203 | params: 1, |
| 5204 | fields: 0, |
| 5205 | ty: nil_ty, |
| 5206 | }, |
| 5207 | ); |
| 5208 | |
| 5209 | // List.cons : ∀ (α : Sort u) (head : α) (tail : List α), List α |
| 5210 | let cons_ty = pi( |
| 5211 | AE::sort(param(0)), |
| 5212 | pi( |
| 5213 | var(0), |
| 5214 | pi( |
| 5215 | app(cnst("List", &[param(0)]), var(1)), |
| 5216 | app(cnst("List", &[param(0)]), var(2)), |
| 5217 | ), |
| 5218 | ), |
| 5219 | ); |
| 5220 | env.insert( |
| 5221 | mk_id("List.cons"), |
| 5222 | KConst::Ctor { |
| 5223 | name: (), |
| 5224 | level_params: (), |
| 5225 | is_unsafe: false, |
| 5226 | lvls: 1, |
| 5227 | induct: mk_id("List"), |
| 5228 | cidx: 1, |
| 5229 | params: 1, |
| 5230 | fields: 2, |
nothing calls this directly
no test coverage detected