Extra definitions on Option
#
This file defines more operations involving Option α
. Lemmas about them are located in other
files under Mathlib.Data.Option
.
Other basic operations on Option
are defined in the core library.
- some: ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : α} {b : β}, r a b → Option.rel r (some a) (some b)
- none: ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop}, Option.rel r none none
Lifts a relation α → β → Prop
to a relation Option α → Option β → Prop
by just adding
none ~ none
.
Instances For
Traverse an object of Option α
with a function f : α → F β
for an applicative F
.
Instances For
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.
Instances For
An elimination principle for Option
. It is a nondependent version of Option.rec
.
Instances For
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 Option.decidableEq
.
Try to use o.isNone
or o.isSome
instead.