mathlib documentation

data.option.defs

Extra definitions on option #

This file defines more operations involving option α. Lemmas about them are located in other files under data.option.. Other basic operations on option are defined in the core library.

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

Cast of option to list. Returns [a] if the input is some a, and [] if it is none.

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 : α → α → α) :
option α → option α → option α

Two arguments failsafe function. Returns f a b if the inputs are some a and some b, and "does nothing" otherwise.

Equations
source
@[protected, instance]
def option.lift_or_get_comm {α : Type u_1} (f : α → α → α) [h : is_commutative α f] :
is_commutative (option α) (option.lift_or_get f)
source
@[protected, instance]
def option.lift_or_get_assoc {α : Type u_1} (f : α → α → α) [h : is_associative α f] :
is_associative (option α) (option.lift_or_get f)
source
@[protected, instance]
def option.lift_or_get_idem {α : Type u_1} (f : α → α → α) [h : is_idempotent α f] :
is_idempotent (option α) (option.lift_or_get f)
source
@[protected, instance]
def option.lift_or_get_is_left_id {α : Type u_1} (f : α → α → α) :
is_left_id (option α) (option.lift_or_get f) none
source
@[protected, 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) :
option α → 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

Lifts a relation α → β → Prop to a relation option α → option β → Prop by just adding none ~ none.

source
@[simp]
def option.pbind {α : Type u_1} {β : Type u_2} (x : option α) :
(Π (a : α), a ∈ x → option β) → option β

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.

Equations
source
@[simp]
def option.pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : Π (a : α), p a → β) (x : option α) :
(∀ (a : α), a ∈ x → p a) → option β

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.

Equations
source
@[simp]
def option.join {α : Type u_1} :
option (option α) → option α

Flatten an option of option, a specialization of mjoin.

Equations
source
@[protected]
def option.traverse {F : Type u → Type v} [applicative F] {α : Type u_1} {β : Type u} (f : α → F β) :
option α → F (option β)
Equations
source
def option.maybe {m : Type u → Type 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
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
source
def option.melim {α β : Type u_1} {m : Type u_1 → Type u_2} [monad m] (x : m (option α)) (y : m β) (z : α → m β) :
m β

A monadic analogue of option.elim.

Equations
source
def option.mget_or_else {α : Type u_1} {m : Type u_1 → Type u_2} [monad m] (x : m (option α)) (y : m α) :
m α

A monadic analogue of option.get_or_else.

Equations