Skip to content

Instantly share code, notes, and snippets.

@jlouis

jlouis/main.idr

Created July 20, 2017 16:00
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 jlouis/da7a6724f59e493ac3ae5f84eb113d6f to your computer and use it in GitHub Desktop.
Save jlouis/da7a6724f59e493ac3ae5f84eb113d6f to your computer and use it in GitHub Desktop.
Download ZIP
Code to explain when to have dessert in minutes
Raw
main.idr
module Main
data MaybeINTHEBLACKHOLE : Type where
YEAH : Nat -> MaybeVOID
NOPE : Void -> MaybeVOID
data Dessert : MaybeINTHEBLACKHOLE -> Type where
Now : Dessert (YEAH 0)
Never : Dessert (NOPE _)
HalfwayBetween : Dessert (YEAH 15)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment