Data.Maybe

Definitions

isNothing : Maybe a -> Bool

Totality: total
Visibility: public export

isJust : Maybe a -> Bool

Totality: total
Visibility: public export

data IsJust : Maybe a -> Type

  Proof that some `Maybe` is actually `Just`

Totality: total
Visibility: public export
Constructor: 

ItIsJust : IsJust (Just x)

Hint: 

Uninhabited (IsJust Nothing)

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

  Decide whether a 'Maybe' is 'Just'

Totality: total
Visibility: public export

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`.

Totality: total
Visibility: public export

fromJust : (v : Maybe a) -> {auto 0 _ : IsJust v} -> a

  Returns the `a` value of a `Maybe a` which is proved `Just`.

Totality: total
Visibility: public export

toMaybe : Bool -> Lazy a -> Maybe a

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

Totality: total
Visibility: public export

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`.

Totality: total
Visibility: public export

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

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

Totality: total
Visibility: export

filter : (a -> Bool) -> Maybe a -> Maybe a

Totality: total
Visibility: public export