mathlib3 documentation

data.option.defs

Extra definitions on option #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} (b : β) (f : α → β) :
option α → β

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

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 = option.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 = bool.tt ↔ o = option.none
source
theorem option.some_inj {α : Type u_1} {a b : α} :
option.some a = option.some b ↔ a = b
source
theorem option.mem_some_iff {α : Type u_1} {a b : α} :
a ∈ option.some b ↔ b = a
source
def option.decidable_eq_none {α : Type u_1} {o : option α} :
decidable (o = option.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
@[reducible]
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 : α} :
(option.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
Instances for option.lift_or_get
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) option.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) option.none
source
inductive option.rel {α : Type u_1} {β : Type u_2} (r : α → β → Prop) :
option α → option β → Prop

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] (y : m β) (z : α → m β) (x : m (option α)) :
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