# Documentation

## Init.Data.Option.Basic

instance Option.instDecidableEq :
{α : Type u_1} → [inst : ] →
Equations
• Option.instDecidableEq = Option.decEqOption✝
instance Option.instBEq :
{α : Type u_1} → [inst : BEq α] → BEq ()
Equations
• Option.instBEq = { beq := Option.beqOption✝ }
def Option.getM {m : Type u_1 → Type u_2} {α : Type u_1} [] :
m α

Lifts an optional value to any Alternative, sending none to failure.

Equations
• x.getM = match x with | none => failure | some a => pure a
Instances For
@[deprecated Option.getM]
def Option.toMonad {m : Type u_1 → Type u_2} {α : Type u_1} [] [] :
m α
Equations
Instances For
@[inline]
def Option.isSome {α : Type u_1} :
Bool

Returns true on some x and false on none.

Equations
Instances For
@[inline, deprecated Option.isSome]
def Option.toBool {α : Type u_1} :
Bool
Equations
• Option.toBool = Option.isSome
Instances For
@[inline]
def Option.isNone {α : Type u_1} :
Bool

Returns true on none and false on some x.

Equations
Instances For
@[inline]
def Option.isEqSome {α : Type u_1} [BEq α] :
αBool

x?.isEqSome y is equivalent to x? == some y, but avoids an allocation.

Equations
• x✝.isEqSome x = match x✝, x with | some a, b => a == b | none, x => false
Instances For
@[inline]
def Option.bind {α : Type u_1} {β : Type u_2} :
(α)
Equations
• x✝.bind x = match x✝, x with | none, x => none | some a, f => f a
Instances For
@[inline]
def Option.bindM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αm ()) (o : ) :
m ()

Runs f on o's value, if any, and returns its result, or else returns none.

Equations
• = match o with | some a => do let __do_liftf a pure __do_lift | x => pure none
Instances For
@[inline]
def Option.mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [] (f : αm β) (o : ) :
m ()

Runs a monadic function f on an optional value. If the optional value is none the function is not called.

Equations
• = match o with | some a => do let __do_liftf a pure (some __do_lift) | x => pure none
Instances For
theorem Option.map_id {α : Type u_1} :
= id
@[inline]
def Option.filter {α : Type u_1} (p : αBool) :

Keeps an optional value only if it satisfies the predicate p.

Equations
• = match x with | some a => if p a = true then some a else none | none => none
Instances For
@[inline]
def Option.all {α : Type u_1} (p : αBool) :
Bool

Checks that an optional value satisfies a predicate p or is none.

Equations
• = match x with | some a => p a | none => true
Instances For
@[inline]
def Option.any {α : Type u_1} (p : αBool) :
Bool

Checks that an optional value is not none and the value satisfies a predicate p.

Equations
Instances For
@[macro_inline]
def Option.orElse {α : Type u_1} :
(Unit)

Implementation of OrElse's <|> syntax for Option.

Equations
• x✝.orElse x = match x✝, x with | some a, x => some a | none, b => b ()
Instances For
instance Option.instOrElse {α : Type u_1} :
Equations
• Option.instOrElse = { orElse := Option.orElse }
@[inline]
def Option.lt {α : Type u_1} (r : ααProp) :
Prop
Equations
Instances For
instance Option.instDecidableRelLt {α : Type u_1} (r : ααProp) [s : ] :
Equations
• = match x✝, x with | none, some val => | some x, some y => s x y | some val, none => | none, none =>
def Option.merge {α : Type u_1} (fn : ααα) :

Take a pair of options and if they are both some, apply the given fn to produce an output. Otherwise act like orElse.

Equations
Instances For
@[simp]
theorem Option.getD_none :
∀ {α : Type u_1} {a : α}, none.getD a = a
@[simp]
theorem Option.getD_some :
∀ {α : Type u_1} {a b : α}, (some a).getD b = a
@[simp]
theorem Option.map_none' {α : Type u_1} {β : Type u_2} (f : αβ) :
Option.map f none = none
@[simp]
theorem Option.map_some' {α : Type u_1} {β : Type u_2} (a : α) (f : αβ) :
Option.map f (some a) = some (f a)
@[simp]
theorem Option.none_bind {α : Type u_1} {β : Type u_2} (f : α) :
none.bind f = none
@[simp]
theorem Option.some_bind {α : Type u_1} {β : Type u_2} (a : α) (f : α) :
(some a).bind f = f a
@[inline]
def Option.elim {α : Type u_1} {β : Sort u_2} :
β(αβ)β

An elimination principle for Option. It is a nondependent version of Option.recOn.

Equations
• x✝¹.elim x✝ x = match x✝¹, x✝, x with | some x, x_1, f => f x | none, y, x => y
Instances For
@[inline]
def Option.get {α : Type u} (o : ) :
o.isSome = trueα

Extracts the value a from an option that is known to be some a for some a.

Equations
• x✝.get x = match x✝, x with | some x, x_1 => x
Instances For
@[inline]
def Option.guard {α : Type u_1} (p : αProp) [] (a : α) :

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

Equations
• = if p a then some a else none
Instances For
@[inline]
def Option.toList {α : Type u_1} :
List α

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

Equations
• x.toList = match x with | none => [] | some a => [a]
Instances For
@[inline]
def Option.toArray {α : Type u_1} :

Cast of Option to Array. Returns #[a] if the input is some a, and #[] if it is none.

Equations
• x.toArray = match x with | none => #[] | some a => #[a]
Instances For
def Option.liftOrGet {α : 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
inductive Option.Rel {α : Type u_1} {β : Type u_2} (r : αβProp) :
Prop

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

• some: ∀ {α : Type u_1} {β : Type u_2} {r : αβProp} {a : α} {b : β}, r a bOption.Rel r (some a) (some b)

If a ~ b, then some a ~ some b

• none: ∀ {α : Type u_1} {β : Type u_2} {r : αβProp}, Option.Rel r none none

none ~ none

Instances For
@[inline]
def Option.join {α : Type u_1} (x : Option ()) :

Flatten an Option of Option, a specialization of joinM.

Equations
• x.join = x.bind id
Instances For
@[inline]
def Option.mapA {m : Type u_1 → Type u_2} [] {α : Type u_3} {β : Type u_1} (f : αm β) :
m ()

Like Option.mapM but for applicative functors.

Equations
• = match x with | none => pure none | some x => some <$> f x Instances For @[inline] def Option.sequence {m : Type u → Type u_1} [] {α : Type u} : Option (m α)m () 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 • x.sequence = match x with | none => pure none | some fn => some <$> fn
Instances For
@[inline]
def Option.elimM {m : Type u_1 → Type u_2} {α : Type u_1} {β : Type u_1} [] (x : m ()) (y : m β) (z : αm β) :
m β

A monadic analogue of Option.elim.

Equations
Instances For
@[inline]
def Option.getDM {m : Type u_1 → Type u_2} {α : Type u_1} [] (x : ) (y : m α) :
m α

A monadic analogue of Option.getD.

Equations
• x.getDM y = match x with | some a => pure a | none => y
Instances For
instance Option.instLawfulBEq (α : Type u_1) [BEq α] [] :
Equations
• =
@[simp]
theorem Option.all_none :
∀ {α : Type u_1} {p : αBool}, Option.all p none = true
@[simp]
theorem Option.all_some :
∀ {α : Type u_1} {p : αBool} {x : α}, Option.all p (some x) = p x
def Option.min {α : Type u_1} [Min α] :

The minimum of two optional values.

Equations
Instances For
instance Option.instMin {α : Type u_1} [Min α] :
Min ()
Equations
• Option.instMin = { min := Option.min }
@[simp]
theorem Option.min_some_some {α : Type u_1} [Min α] {a : α} {b : α} :
min (some a) (some b) = some (min a b)
@[simp]
theorem Option.min_some_none {α : Type u_1} [Min α] {a : α} :
min (some a) none = some a
@[simp]
theorem Option.min_none_some {α : Type u_1} [Min α] {b : α} :
min none (some b) = some b
@[simp]
theorem Option.min_none_none {α : Type u_1} [Min α] :
min none none = none
def Option.max {α : Type u_1} [Max α] :

The maximum of two optional values.

Equations
Instances For
instance Option.instMax {α : Type u_1} [Max α] :
Max ()
Equations
• Option.instMax = { max := Option.max }
@[simp]
theorem Option.max_some_some {α : Type u_1} [Max α] {a : α} {b : α} :
max (some a) (some b) = some (max a b)
@[simp]
theorem Option.max_some_none {α : Type u_1} [Max α] {a : α} :
max (some a) none = some a
@[simp]
theorem Option.max_none_some {α : Type u_1} [Max α] {b : α} :
max none (some b) = some b
@[simp]
theorem Option.max_none_none {α : Type u_1} [Max α] :
max none none = none
instance instLTOption {α : Type u_1} [LT α] :
LT ()
Equations
• instLTOption = { lt := Option.lt fun (x x_1 : α) => x < x_1 }
@[always_inline]
Equations
@[always_inline]
Equations
@[always_inline]
Equations
def liftOption {m : Type u_1 → Type u_2} {α : Type u_1} [] :
m α
Equations
• = match x with | some a => pure a | none => failure
Instances For
@[inline]
def Option.tryCatch {α : Type u_1} (x : ) (handle : Unit) :
Equations
• x.tryCatch handle = match x with | some val => x | none => handle ()
Instances For
Equations