An elimination principle for Option
. It is a nondependent version of Option.recOn
.
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 instance : DecidableEq Option
.
Try to use o.isNone
or o.isSome
instead.
Instances For
- 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
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
.
Instances For
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
.
Instances For
Like Option.mapM
but for applicative functors.
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
A monadic analogue of Option.elim
.