mathlib documentation

data.option.defs

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

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

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

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

theorem option.is_none_iff_eq_none {α : Type u_1} {o : option α} :

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

def option.decidable_eq_none {α : Type u_1} {o : option α} :

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

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

Equations
def option.iget {α : Type u_1} [inhabited α] :
option α → α

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

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

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

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

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

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

Equations
def option.to_list {α : Type u_1} :
option αlist α

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

def option.lift_or_get {α : Type u_1} :
(α → α → α)option αoption αoption α

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

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

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

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

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

inductive option.rel {α : Type u_1} {β : Type u_2} :
(α → β → Prop)option αoption β → Prop
  • some : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop) {a : α} {b : β}, r a boption.rel r (some a) (some b)
  • none : ∀ {α : Type u_1} {β : Type u_2} (r : α → β → Prop), option.rel r none none

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

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

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

Equations