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

ink

inductive Option.rel {α : Type u_1} {β : Type u_2} (r : α → β → Prop) :

Option α → Option β → Prop

If a ~ b, then some a ~ some b
some: ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop} {a : α} {b : β}, r a b → Option.rel r (some a) (some b)
none ~ none
none: ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop}, Option.rel r none none

Lifts a relation α → β → Prop→ β → Prop→ Prop to a relation Option α → Option β → Prop→ Option β → Prop→ Prop by just adding none ~ none.

Instances For

source

ink

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

Option α → F (Option β)

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

Equations

Option.traverse f x = match x with | none => pure none | some x => some <$> f x

source

ink

def Option.maybe {m : Type u → Type v} [inst : 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

Option.maybe x = match x with | none => pure none | some fn => some <$> fn

source

ink

def Option.getDM' {m : Type u_1 → Type u_2} {α : Type u_1} [inst : Monad m] (x : m (Option α)) (y : m α) :

m α

Equations

Option.getDM' x y = do let __do_lift ← x Option.getDM __do_lift y

source

ink

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 x = match x with | some a => f a | none => b

source

ink

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

a ∈ some b ↔ b = a

source

ink

@[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