Agda.Utils.Maybe.Strict

Analogous to L.catMaybes in Data.Maybe.

Extracts the element out of a Just and throws an error if the argument is Nothing.

Given a default value and a Maybe, yield the default value if the Maybe argument is Nothing and extract the value out of the Just otherwise.

Yields True iff the argument is of the form Just _.

Yields True iff the argument is Nothing.

Analogous to L.listToMaybe in Data.Maybe.

Analogous to L.mapMaybe in Data.Maybe.

Given a default value, a function and a Maybe value, yields the default value if the Maybe value is Nothing and applies the function to the value stored in the Just otherwise.

Analogous to L.maybeToList in Data.Maybe.

The type of strict optional values.

Ad hoc conversion between "strict" and "lazy" versions of a structure.

Unfortunately all externally defined instances are doomed to be orphans: https://gitlab.haskell.org/ghc/ghc/-/issues/11999 See also https://qfpl.io/posts/orphans-and-fundeps/index.html for

Version of maybe with different argument ordering. Often, we want to case on a Maybe, do something interesting in the Just case, but only a default action in the Nothing case. Then, the argument ordering of caseMaybe is preferable.

caseMaybe m err f = flip (maybe err) m f

Monadic version of caseMaybe. That is, maybeM with a different argument ordering.

Filtering a singleton list.

filterMaybe p a = listToMaybe (filter p [a])

Version of mapMaybe with different argument ordering.

Monadic version of fromMaybe.

caseMaybeM with flipped branches.

Monadic version of maybe.

unionWith for collections of size <= 1.

Unzipping a list of length <= 1.

A more telling name for Traversable.forM for the Maybe collection type. Or: caseMaybe without the Nothing case.

caseMaybeM without the Nothing case.