mathlib documentation

data.option.defs

source
@[simp]
def option.elim {α : Type u_1} {β : Type u_2} (a : option α) (a_1 : β) (a_2 : α → β) :
β

An elimination principle for option. It is a nondependent version of option.rec_on.

Equations
source
@[instance]
def option.has_mem {α : Type u_1} :
has_mem α (option α)

Equations
source
@[simp]
theorem option.mem_def {α : Type u_1} {a : α} {b : option α} :
a ∈ b ↔ b = some a

source
theorem option.is_none_iff_eq_none {α : Type u_1} {o : option α} :
o.is_none = tt ↔ o = none

source
theorem option.some_inj {α : Type u_1} {a b : α} :
some a = some b ↔ a = b

source
def option.decidable_eq_none {α : Type u_1} {o : option α} :
decidable (o = none)

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
source
@[instance]
def option.decidable_forall_mem {α : Type u_1} {p : α → Prop} [decidable_pred p] (o : option α) :
decidable (∀ (a : α), a ∈ o → p a)

Equations
source
@[instance]
def option.decidable_exists_mem {α : Type u_1} {p : α → Prop} [decidable_pred p] (o : option α) :
decidable (∃ (a : α) (H : a ∈ o), p a)

Equations
source
def option.iget {α : Type u_1} [inhabited α] (a : option α) :
α

inhabited get function. Returns a if the input is some a, otherwise returns default.

Equations
source
@[simp]
theorem option.iget_some {α : Type u_1} [inhabited α] {a : α} :
(some a).iget = a

source
def option.guard {α : Type u_1} (p : α → Prop) [decidable_pred p] (a : α) :
option α

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

Equations
source
def option.filter {α : Type u_1} (p : α → Prop) [decidable_pred p] (o : option α) :
option α

filter p o returns some a if o is some a and p a holds, otherwise none.

Equations
source
def option.to_list {α : Type u_1} (a : option α) :
list α

Equations
source
@[simp]
theorem option.mem_to_list {α : Type u_1} {a : α} {o : option α} :
a ∈ o.to_list ↔ a ∈ o

source
def option.lift_or_get {α : Type u_1} (f : α → α → α) (a a_1 : option α) :
option α

Equations
source
@[instance]
def option.lift_or_get_comm {α : Type u_1} (f : α → α → α) [h : is_commutative α f] :
is_commutative (option α) (option.lift_or_get f)

source
@[instance]
def option.lift_or_get_assoc {α : Type u_1} (f : α → α → α) [h : is_associative α f] :
is_associative (option α) (option.lift_or_get f)

source
@[instance]
def option.lift_or_get_idem {α : Type u_1} (f : α → α → α) [h : is_idempotent α f] :
is_idempotent (option α) (option.lift_or_get f)

source
@[instance]
def option.lift_or_get_is_left_id {α : Type u_1} (f : α → α → α) :
is_left_id (option α) (option.lift_or_get f) none

source
@[instance]
def option.lift_or_get_is_right_id {α : Type u_1} (f : α → α → α) :
is_right_id (option α) (option.lift_or_get f) none

source
inductive option.rel {α : Type u_1} {β : Type u_2} (r : α → β → Prop) (a : option α) (a_1 : option β) :
Prop
  • 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

source
def option.traverse {F : Type u → Type v} [applicative F] {α : Type u_1} {β : Type u} (f : α → F β) (a : option α) :
F (option β)

Equations
source
def option.maybe {m : Type u → Type v} [monad m] {α : Type u} (a : option (m α)) :
m (option α)

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
source
def option.mmap {m : Type u → Type v} [monad m] {α : Type w} {β : Type u} (f : α → m β) (o : option α) :
m (option β)

Map a monadic function f : α → m β over an o : option α, maybe producing a result.

Equations