core / init.data.option.basic

source

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

option A → m A

Equations

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

source

def option.get_or_else {α : Type u} :

option α → α → α

Equations

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

source

def option.is_some {α : Type u} :

option α → bool

Equations

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

source

def option.is_none {α : Type u} :

option α → bool

Equations

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

source

def option.get {α : Type u} {o : option α} :

↥(o.is_some) → α

Equations

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

source

def option.rhoare {α : Type u} :

bool → α → option α

Equations

(bool.tt |>a) = option.none
(bool.ff |>a) = option.some a

source

def option.lhoare {α : Type u} :

α → option α → α

Equations

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

source

@[protected]

def option.bind {α : Type u} {β : Type v} :

option α → (α → option β) → option β

Equations

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

source

@[protected]

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

option β

Equations

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

source

@[simp]

theorem option.map_id {α : Type u_1} :

option.map id = id

source

@[protected, instance]

def option.monad :

monad option

Equations

option.monad = monad.mk

source

@[protected]

def option.orelse {α : Type u} :

option α → option α → option α

Equations

(option.some a).orelse o = option.some a
option.none.orelse (option.some a) = option.some a
option.none.orelse option.none = option.none

source

@[protected, 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), has_pure.pure x <*> y, map_const := λ (α β : Type u_1), (λ (x : β → α) (y : option β), has_pure.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), has_pure.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), has_pure.pure x <*> y) α (β → β) (function.const α id) a <*> b}}, to_has_orelse := {orelse := option.orelse}, failure := option.none}

source

@[protected, instance]

def option.inhabited (α : Type u) :

inhabited (option α)

Equations

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

source

@[protected, instance]

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

decidable_eq (option α)

Equations

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