Extra definitions on `Option` #

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

source

def Option.traverse {F : Type u → Type v} [Applicative F] {α : Type u_1} {β : Type u} (f : α → F β) :

Option α → F (Option β)

Traverse an object of Option α with a function f : α → F β for an applicative F.

Equations

Option.traverse f none = pure none
Option.traverse f (some x_1) = some <$> f x_1

Instances For

source

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

Option.elim' b f (some a) = f a
Option.elim' b f none = b

Instances For

source

@[simp]

theorem Option.elim'_none {α : Type u_1} {β : Type u_2} (b : β) (f : α → β) :

Option.elim' b f none = b

source

@[simp]

theorem Option.elim'_some {α : Type u_1} {β : Type u_2} {a : α} (b : β) (f : α → β) :

Option.elim' b f (some a) = f a

source

@[simp]

theorem Option.elim'_none_some {α : Type u_1} {β : Type u_2} (f : Option α → β) :

Option.elim' (f none) (f ∘ some) = f

source

theorem Option.elim'_eq_elim {α : Type u_3} {β : Type u_4} (b : β) (f : α → β) (a : Option α) :

Option.elim' b f a = a.elim b f

source

theorem Option.mem_some_iff {α : Type u_3} {a b : α} :

a ∈ some b ↔ b = a

source

@[inline]

def Option.decidableEqNone {α : 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.decidableEq. Try to use o.isNone or o.isSome instead.

Equations