data Bool () where { True : Bool () False : Bool () }; data Maybe ('a) where { Nothing : Maybe ('a) Just : 'a -> Maybe ('a) }; main : Bool () -> Maybe (Bool ()) ; main x = case x of { True => Nothing; False => Just 0 }