mathlib docs: core.init.data.option.basic

source

def option.to_monad {m : Type → Type} [monad m] [alternative m] {A : Type} (a : option A) :

m A

Equations

(some a).to_monad = return a
none.to_monad = failure

source

def option.get_or_else {α : Type u} (a : option α) (a_1 : α) :

α

Equations

(some x).get_or_else _x = x
none.get_or_else e = e

source

def option.is_some {α : Type u} (a : option α) :

bool

Equations

(some _x).is_some = tt
none.is_some = ff

source

def option.is_none {α : Type u} (a : option α) :

bool

Equations

(some _x).is_none = ff
none.is_none = tt

source

def option.get {α : Type u} {o : option α} (a : ↥(o.is_some)) :

α

Equations

option.get h = x
option.get h = false.rec α _

source

def option.rhoare {α : Type u} (a : bool) (a_1 : α) :

option α

Equations

(tt |>a) = none
(ff |>a) = some a

source

def option.lhoare {α : Type u} (a : α) (a_1 : option α) :

α

Equations

(_x<|some b) = b
(a<|none) = a

source

def option.bind {α : Type u} {β : Type v} (a : option α) (a_1 : α → option β) :

option β

Equations

(some a).bind b = b a
none.bind b = none

source

def option.map {α : Type u_1} {β : Type u_2} (f : α → β) (o : option α) :

option β

Equations

option.map f o = o.bind (some ∘ f)

source

theorem option.map_id {α : Type u_1} :

option.map id = id

source

@[instance]

def option.monad :

monad option

Equations

option.monad = monad.mk

source

def option.orelse {α : Type u} (a a_1 : option α) :

option α

Equations

source

@[instance]

def option.alternative :

alternative option

Equations

option.alternative = {to_applicative := {to_functor := {map := λ (_x _x_1 : Type u_1) (x : _x → _x_1) (y : option _x), pure x <*> y, map_const := λ (α β : Type u_1), (λ (x : β → α) (y : option β), pure x <*> y) ∘ function.const β}, to_has_pure := applicative.to_has_pure monad.to_applicative, to_has_seq := applicative.to_has_seq monad.to_applicative, to_has_seq_left := {seq_left := λ (α β : Type u_1) (a : option α) (b : option β), (λ (_x _x_1 : Type u_1) (x : _x → _x_1) (y : option _x), pure x <*> y) α (β → α) (function.const β) a <*> b}, to_has_seq_right := {seq_right := λ (α β : Type u_1) (a : option α) (b : option β), (λ (_x _x_1 : Type u_1) (x : _x → _x_1) (y : option _x), pure x <*> y) α (β → β) (function.const α id) a <*> b}}, to_has_orelse := {orelse := option.orelse}, failure := none}

source

@[instance]

def option.inhabited (α : Type u) :

inhabited (option α)

Equations

option.inhabited α = {default := none α}

source

@[instance]

def option.decidable_eq {α : Type u} [d : decidable_eq α] :

decidable_eq (option α)

Equations

option.decidable_eq (some v₁) (some v₂) = option.decidable_eq._match_1 v₁ v₂ (d v₁ v₂)
option.decidable_eq (some v₁) none = is_false _
option.decidable_eq none (some v₂) = is_false _
option.decidable_eq none none = is_true option.decidable_eq._main._proof_1
option.decidable_eq._match_1 v₁ v₂ (is_true e) = is_true _
option.decidable_eq._match_1 v₁ v₂ (is_false n) = is_false _