Skip to content

Instantly share code, notes, and snippets.

Created July 20, 2017 16:00
What would you like to do?
Code to explain when to have dessert in minutes
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