Idris2Doc : Data.Maybe

Data.Maybe

dataIsJust : Maybea -> Type
  Proof that some `Maybe` is actually `Just`

Totality: total
Constructor: 
ItIsJust : IsJust (Justx)
filter : (a -> Bool) -> Maybea -> Maybea
Totality: total
fromJust : (v : Maybea) -> {auto 0 _ : IsJustv} -> a
  Returns the `a` value of a `Maybe a` which is proved `Just`.

Totality: total
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`.

Totality: total
isItJust : (v : Maybea) -> Dec (IsJustv)
  Decide whether a 'Maybe' is 'Just'

Totality: total
isJust : Maybea -> Bool
Totality: total
isNothing : Maybea -> Bool
Totality: total
justInjective : Justx = Justy -> x = y
Totality: total
lowerMaybe : Monoida => Maybea -> a
  Convert a `Maybe a` value to an `a` value, using `neutral` in the case
that the `Maybe` value is `Nothing`.

Totality: total
raiseToMaybe : (Monoida, Eqa) => a -> Maybea
  Returns `Nothing` when applied to `neutral`, and `Just` the value otherwise.

Totality: total
toMaybe : Bool -> Lazy a -> Maybea
  Returns `Just` the given value if the conditional is `True`
and `Nothing` if the conditional is `False`.

Totality: total