Skip to content

Instantly share code, notes, and snippets.

@david-christiansen

david-christiansen/gist:4994451

Created February 20, 2013 10:12
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save david-christiansen/4994451 to your computer and use it in GitHub Desktop.
Save david-christiansen/4994451 to your computer and use it in GitHub Desktop.
Download ZIP
HList demo
Raw
gistfile1.txt
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
Copy link
Author

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