Idris2Doc : Data.Maybe

Data.Maybe

IsJust : Maybea -> Type
Proof that some `Maybe` is actually `Just`
Totality: total
Constructor: 
ItIsJust : IsJust (Justx)
filter : (a -> Bool) -> Maybea -> Maybea
fromJust : (v : Maybea) -> {auto 0 _ : IsJustv} -> a
Returns the `a` value of a `Maybe a` which is proved `Just`.
fromMaybe : Lazy a -> Maybea -> 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 : Maybea) -> Dec (IsJustv)
Decide whether a 'Maybe' is 'Just'
isJust : Maybea -> Bool
isNothing : Maybea -> Bool
justInjective : Justx = Justy -> x = y
lowerMaybe : Monoida => Maybea -> a
Convert a `Maybe a` value to an `a` value, using `neutral` in the case
that the `Maybe` value is `Nothing`.
raiseToMaybe : (Monoida, Eqa) => a -> Maybea
Returns `Nothing` when applied to `neutral`, and `Just` the value otherwise.
toMaybe : Bool -> Lazy a -> Maybea
Returns `Just` the given value if the conditional is `True`
and `Nothing` if the conditional is `False`.