Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
HList demo
module HList
%default total
data HList : List Type -> Type where
(::) : t -> (xs : HList ts) -> HList (t :: ts)
Nil : HList []
foo : HList [Int, String, Int]
foo = [3, "yes", 17]
@david-christiansen

This comment has been minimized.

Copy link
Owner Author

@david-christiansen david-christiansen commented Feb 20, 2013

Output:

Type checking ./HList.idr
*HList> foo
HList.:: 3 (HList.:: "yes" (HList.:: 17 HList.Nil)) : HList (Prelude.List.:: Int (Prelude.List.:: String (Prelude.List.:: Int (Prelude.List.Nil))))
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.