Extracts the value a from an option that is known to be some a for some a.

Get with default. If opt : Option α and dflt : α, then opt.getD dflt returns a if opt = some a and dflt otherwise.

This function is @[macro_inline], so dflt will not be evaluated unless opt turns out to be none.

A monadic analogue of Option.getD.

Lifts an optional value to any Alternative, sending none to failure.

An elimination principle for Option. It is a nondependent version of Option.recOn.

A monadic analogue of Option.elim.

Two arguments failsafe function. Returns f a b if the inputs are some a and some b, and "does nothing" otherwise.

Take a pair of options and if they are both some, apply the given fn to produce an output. Otherwise act like orElse.

Returns true on none and false on some x.

Returns true on some x and false on none.

x?.isEqSome y is equivalent to x? == some y, but avoids an allocation.

The minimum of two optional values.

The maximum of two optional values.

o = none is decidable even if the wrapped type does not have decidable equality. This is not an instance because it is not definitionally equal to instance : DecidableEq Option. Try to use o.isNone or o.isSome instead.

Cast of Option to Array. Returns #[a] if the input is some a, and #[] if it is none.

Cast of Option to List. Returns [a] if the input is some a, and [] if it is none.

guard p a returns some a if p a holds, otherwise none.

Runs f on o's value, if any, and returns its result, or else returns none.

Flatten an Option of Option, a specialization of joinM.

If you maybe have a monadic computation in a [Monad m] which produces a term of type α, then there is a naturally associated way to always perform a computation in m which maybe produces a result.

If the first argument is some a, returns some a, otherwise returns the second argument. This is similar to <|>/orElse, but it is strict in the second argument.

Implementation of OrElse's <|> syntax for Option. If the first argument is some a, returns some a, otherwise evaluates and returns the second argument. See also or for a version that is strict in the second argument.

Checks that an optional value satisfies a predicate p or is none.

Checks that an optional value is not none and the value satisfies a predicate p.

Keeps an optional value only if it satisfies the predicate p.

Map a monadic function which returns Unit over an Option.

Map a function over an Option by applying the function to the contained value if present.

Like Option.mapM but for applicative functors.

Runs a monadic function f on an optional value. If the optional value is none the function is not called.

"Attach" the proof that the element of xs, if present, is in xs to produce a new option with the same elements but in the type {x // x ∈ xs}.

"Attach" a proof P x that holds for the element of o, if present, to produce a new option with the same element but in the type {x // P x}.

A synonym for l.map (·.val). Mostly this should not be needed by users. It is introduced as an intermediate step by lemmas such as map_subtype, and is ideally subsequently simplified away by unattach_attach.

If not, usually the right approach is simp [Option.unattach, -Option.map_subtype] to unfold.

An arbitrary some a with a : α if α is nonempty, and otherwise none.

Partial bind. If for some x : Option α, f : Π (a : α), a ∈ x → Option β is a partial function defined on a : α giving an Option β, where some a = x, then pbind x f h is essentially the same as bind x f but is defined only when all x = some a, using the proof to apply f.

Partial elimination. If o : Option α and f : (a : α) → a ∈ o → β, then o.pelim b f is the same as o.elim b f but f is passed the proof that a ∈ o.

Partial map. If f : Π a, p a → β is a partial function defined on a : α satisfying p, then pmap f x h is essentially the same as map f x but is defined only when all members of x satisfy p, using the proof to apply f.