{-# LANGUAGE UnboxedSums #-} {-# LANGUAGE UnboxedTuples #-} {-# LANGUAGE MagicHash #-} module Agda.Utils.Maybe.Unboxable where data Maybe# a = Maybe# (# a | (# #) #) pattern Nothing# :: Maybe# a pattern $mNothing# :: forall {r} {a}. Maybe# a -> ((# #) -> r) -> ((# #) -> r) -> r $bNothing# :: forall a. Maybe# a Nothing# = Maybe# (# | (# #) #) pattern Just# :: a -> Maybe# a pattern $mJust# :: forall {r} {a}. Maybe# a -> (a -> r) -> ((# #) -> r) -> r $bJust# :: forall a. a -> Maybe# a Just# a = Maybe# (# a | #) {-# COMPLETE Nothing#, Just# #-}