Prelude.Maybe

data IsJust : Maybe a -> Type

Proof that some Maybe is actually Just

ItIsJust : IsJust (Just x)

data Maybe : (a : Type) -> Type

An optional value. This can be used to represent the possibility of
failure, where a function may return a value, or not.

Nothing : Maybe a

No value stored

Just : (x : a) -> Maybe a

A value of type a is stored

collectJust : Semigroup a => Semigroup (Maybe a)

Transform any semigroup into a monoid by using Nothing as the
designated neutral element and collecting the contents of the
Just constructors using a semigroup structure on a. This is
the behaviour in the Haskell libraries.

fromMaybe : Lazy a -> Maybe a -> a

Convert a Maybe a value to an a value by providing a default a value
in the case that the Maybe value is Nothing.

isItJust : (v : Maybe a) -> Dec (IsJust v)

Decide whether a 'Maybe' is 'Just'

isJust : Maybe a -> Bool

isNothing : Maybe a -> Bool

justInjective : (Just x = Just y) -> x = y

lowerMaybe : Monoid a => Maybe a -> a

Convert a Maybe a value to an a value, using neutral in the case
that the Maybe value is Nothing.

maybe : Lazy b -> Lazy (a -> b) -> Maybe a -> b

maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b

raiseToMaybe : Monoid a => Eq a => a -> Maybe a

Returns Nothing when applied to neutral, and Just the value otherwise.

toMaybe : Bool -> Lazy a -> Maybe a

Returns Just the given value if the conditional is True
and Nothing if the conditional is False.