Code to explain when to have dessert in minutes

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)