An elimination principle for option. It is a nondependent version of option.rec_on.
Equations
- (option.some x).elim y f = f x
- option.none.elim y f = y
Equations
- option.has_mem = {mem := λ (a : α) (b : option α), b = option.some a}
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.decidable_eq.
Try to use o.is_none or o.is_some instead.
Equations
- (option.some a).decidable_forall_mem = dite (p a) (λ (h : p a), decidable.is_true _) (λ (h : ¬p a), decidable.is_false _)
- option.none.decidable_forall_mem = decidable.is_true option.decidable_forall_mem._main._proof_1
Equations
- (option.some a).decidable_exists_mem = dite (p a) (λ (h : p a), decidable.is_true _) (λ (h : ¬p a), decidable.is_false _)
- option.none.decidable_exists_mem = decidable.is_false option.decidable_exists_mem._main._proof_1
inhabited get function. Returns a if the input is some a,
otherwise returns default.
Equations
- (option.some x).iget = x
- option.none.iget = inhabited.default α
guard p a returns some a if p a holds, otherwise none.
Equations
- option.guard p a = ite (p a) (option.some a) option.none
filter p o returns some a if o is some a
and p a holds, otherwise none.
Equations
- option.filter p o = o.bind (option.guard p)
Equations
- (option.some a).to_list = [a]
- option.none.to_list = list.nil
Equations
- option.lift_or_get f (option.some a) (option.some b) = option.some (f a b)
- option.lift_or_get f (option.some a) option.none = option.some a
- option.lift_or_get f option.none (option.some b) = option.some b
- option.lift_or_get f option.none option.none = option.none
Equations
- _ = _
Equations
- _ = _
Equations
- _ = _
- some : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) {a : α} {b : β}, r a b → option.rel r (option.some a) (option.some b)
- none : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop), option.rel r option.none option.none
Equations
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.
Equations
- (option.some fn).maybe = option.some <$> fn
- option.none.maybe = return option.none
Map a monadic function f : α → m β over an o : option α, maybe producing a result.
Equations
- option.mmap f o = (option.map f o).maybe