module Data.Maybe public exportisNothing : Maybe a -> BoolisNothing Nothing  = TrueisNothing (Just j) = False public exportisJust : Maybe a -> BoolisJust Nothing  = FalseisJust (Just j) = True ||| Proof that some `Maybe` is actually `Just`public exportdata IsJust : Maybe a -> Type where  ItIsJust : IsJust (Just x) exportUninhabited (IsJust Nothing) where  uninhabited ItIsJust impossible ||| Decide whether a 'Maybe' is 'Just'public exportisItJust : (v : Maybe a) -> Dec (IsJust v)isItJust (Just x) = Yes ItIsJustisItJust Nothing = No absurd ||| Convert a `Maybe a` value to an `a` value by providing a default `a` value||| in the case that the `Maybe` value is `Nothing`.public exportfromMaybe : (Lazy a) -> Maybe a -> afromMaybe def Nothing  = deffromMaybe def (Just j) = j ||| Returns `Just` the given value if the conditional is `True`||| and `Nothing` if the conditional is `False`.public exporttoMaybe : Bool -> Lazy a -> Maybe atoMaybe True  j = Just jtoMaybe False j = Nothing exportjustInjective : {x : t} -> {y : t} -> (Just x = Just y) -> x = yjustInjective Refl = Refl ||| Convert a `Maybe a` value to an `a` value, using `neutral` in the case||| that the `Maybe` value is `Nothing`.public exportlowerMaybe : Monoid a => Maybe a -> alowerMaybe Nothing = neutrallowerMaybe (Just x) = x ||| Returns `Nothing` when applied to `neutral`, and `Just` the value otherwise.exportraiseToMaybe : (Monoid a, Eq a) => a -> Maybe araiseToMaybe x = if x == neutral then Nothing else Just x