mathlib documentation

data.option.defs

Extra definitions on option #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. https://github.com/leanprover-community/mathlib4/pull/504 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.

@[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
@[protected, instance]
def option.has_mem {α : Type u_1} :
has_mem α (option α)
Equations
@[simp]
theorem option.mem_def {α : Type u_1} {a : α} {b : option α} :
theorem option.mem_iff {α : Type u_1} {a : α} {b : option α} :
a b b = a
theorem option.some_inj {α : Type u_1} {a b : α} :
theorem option.mem_some_iff {α : Type u_1} {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
@[protected, instance]
def option.decidable_forall_mem {α : Type u_1} {p : α Prop} [decidable_pred p] (o : option α) :
decidable ( (a : α), a o p a)
Equations
@[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
@[reducible]
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 : α} :
def option.guard {α : Type u_1} (p : α Prop) [decidable_pred p] (a : α) :

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

Equations
def option.filter {α : Type u_1} (p : α Prop) [decidable_pred p] (o : 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} :

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

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} (f : α α α) :

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

@[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
@[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
@[simp]
def option.join {α : Type u_1} :

Flatten an option of option, a specialization of mjoin.

Equations
@[protected]
def option.traverse {F : Type u Type v} [applicative F] {α : Type u_1} {β : Type u} (f : α F β) :
option α F (option β)
Equations
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
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
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
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