| inductive HList {α : Type v} (β : α → Type u) : List α → Type (max u v) | |
| | nil : HList β [] | |
| | cons : β i → HList β is → HList β (i::is) | |
| infix:67 " :: " => HList.cons | |
| inductive Member : α → List α → Type | |
| | head : Member a (a::as) | |
| | tail : Member a bs → Member a (b::bs) | |
| def HList.get : HList β is → Member i is → β i | |
| | a::as, .head => a | |
| | a::as, .tail h => as.get _ |