Skip to content

Instantly share code, notes, and snippets.

@jlouis

jlouis/main.idr

Created July 20, 2017 16:00
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Embed
What would you like to do?
Learn more about clone URLs
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