Init.Data.Option.Basic

Implementation of OrElse's <|> syntax for Option. If the first argument is some a, returns some a, otherwise evaluates and returns the second argument. See also or for a version that is strict in the second argument.

Equations

(some a).orElse x✝ = some a
none.orElse x✝ = x✝ ()

source

instance Option.instOrElse {α : Type u_1} :

OrElse (Option α)

Equations

Option.instOrElse = { orElse := Option.orElse }

source

@[macro_inline]

def Option.or {α : Type u_1} :

Option α → Option α → Option α

If the first argument is some a, returns some a, otherwise returns the second argument. This is similar to <|>/orElse, but it is strict in the second argument.

Equations

(some a).or x✝ = some a
none.or x✝ = x✝

Instances For

source

@[inline]

def Option.lt {α : Type u_1} {β : Type u_2} (r : α → β → Prop) :

Option α → Option β → Prop

Equations

Option.lt r none (some val) = True
Option.lt r (some x_2) (some y) = r x_2 y
Option.lt r x✝¹ x✝ = False

Instances For

Option.instDecidableRelLt

source

@[inline]

def Option.le {α : Type u_1} {β : Type u_2} (r : α → β → Prop) :

Option α → Option β → Prop

Equations

Option.le r none (some val) = True
Option.le r none none = True
Option.le r (some val) none = False
Option.le r (some x_2) (some y) = r x_2 y

source

instance Option.instDecidableRelLt {α : Type u_1} {β : Type u_2} (r : α → β → Prop) [s : DecidableRel r] :

DecidableRel (Option.lt r)

Equations

Option.instDecidableRelLt r none (some val) = isTrue trivial
Option.instDecidableRelLt r (some x_2) (some y) = s x_2 y
Option.instDecidableRelLt r (some val) none = isFalse not_false
Option.instDecidableRelLt r none none = isFalse not_false

source

def Option.merge {α : Type u_1} (fn : α → α → α) :

Option α → Option α → Option α

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

Equations

Option.merge fn none none = none
Option.merge fn (some x_2) none = some x_2
Option.merge fn none (some y) = some y
Option.merge fn (some x_2) (some y) = some (fn x_2 y)

source

@[simp]

theorem Option.getD_none {α✝ : Type u_1} {a : α✝} :

none.getD a = a

source

@[simp]

theorem Option.getD_some {α✝ : Type u_1} {a b : α✝} :

(some a).getD b = a

source

@[simp]

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

Option.map f none = none

source

@[simp]

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

Option.map f (some a) = some (f a)

source

@[simp]

theorem Option.none_bind {α : Type u_1} {β : Type u_2} (f : α → Option β) :

none.bind f = none

source

@[simp]

theorem Option.some_bind {α : Type u_1} {β : Type u_2} (a : α) (f : α → Option β) :

(some a).bind f = f a

source

@[inline]

def Option.elim {α : Type u_1} {β : Sort u_2} :

Option α → β → (α → β) → β

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

Equations

(some x_3).elim x✝¹ x✝ = x✝ x_3
none.elim x✝¹ x✝ = x✝¹

source

@[inline]

def Option.get {α : Type u} (o : Option α) :

o.isSome = true → α

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

Equations

(some x_2).get x_3 = x_2

source

@[simp]

theorem Option.some_get {α : Type u_1} {x : Option α} (h : x.isSome = true) :

some (x.get h) = x

source

@[simp]

theorem Option.get_some {α : Type u_1} (x : α) (h : (some x).isSome = true) :

(some x).get h = x

source

@[inline]

def Option.guard {α : Type u_1} (p : α → Prop) [DecidablePred p] (a : α) :

Option α

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

Equations

Option.guard p a = if p a then some a else none

source

@[inline]

def Option.toList {α : Type u_1} :

Option α → List α

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

Equations

none.toList = []
(some a).toList = [a]

source

@[inline]

def Option.toArray {α : Type u_1} :

Option α → Array α

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

Equations

none.toArray = #[]
(some a).toArray = #[a]

source

def Option.liftOrGet {α : Type u_1} (f : α → α → α) :

Option α → Option α → Option α

Two arguments failsafe function. Returns f a b if the inputs are some a and some b, and "does nothing" otherwise.

Equations

Option.liftOrGet f none none = none
Option.liftOrGet f (some x_2) none = some x_2
Option.liftOrGet f none (some y) = some y
Option.liftOrGet f (some x_2) (some y) = some (f x_2 y)

Instances For

source

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

Option α → Option β → 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 b → Rel r (Option.some a) (Option.some b)
If a ~ b, then some a ~ some b
none {α : Type u_1} {β : Type u_2} {r : α → β → Prop} : Rel r Option.none Option.none
none ~ none

source

@[inline]

def Option.join {α : Type u_1} (x : Option (Option α)) :

Option α

Flatten an Option of Option, a specialization of joinM.

Equations

x.join = x.bind id

source

@[inline]

def Option.mapA {m : Type u_1 → Type u_2} [Applicative m] {α : Type u_3} {β : Type u_1} (f : α → m β) :

Option α → m (Option β)

Like Option.mapM but for applicative functors.

Equations

Option.mapA f none = pure none
Option.mapA f (some a) = some <$> f a

source

@[inline]

def Option.sequence {m : Type u → Type u_1} [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

none.sequence = pure none
(some fn).sequence = some <$> fn

source

@[inline]

def Option.elimM {m : Type u_1 → Type u_2} {α β : Type u_1} [Monad m] (x : m (Option α)) (y : m β) (z : α → m β) :

m β

A monadic analogue of Option.elim.

Equations

Option.elimM x y z = do let __do_lift ← x __do_lift.elim y z

source

@[inline]

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

m α

A monadic analogue of Option.getD.

Equations

(some val).getDM y = pure val
none.getDM y = y

source

instance Option.instLawfulBEq (α : Type u_1) [BEq α] [LawfulBEq α] :

LawfulBEq (Option α)

source

@[simp]

theorem Option.all_none {α✝ : Type u_1} {p : α✝ → Bool} :

Option.all p none = true

source

@[simp]

theorem Option.all_some {α✝ : Type u_1} {p : α✝ → Bool} {x : α✝} :

Option.all p (some x) = p x

source

@[simp]

theorem Option.any_none {α✝ : Type u_1} {p : α✝ → Bool} :

Option.any p none = false

source

@[simp]

theorem Option.any_some {α✝ : Type u_1} {p : α✝ → Bool} {x : α✝} :

Option.any p (some x) = p x

source

def Option.min {α : Type u_1} [Min α] :

Option α → Option α → Option α

The minimum of two optional values.

Note this treats none as the least element, so min none x = min x none = none for all x : Option α. Prior to nightly-2025-02-27, we instead had min none (some x) = min (some x) none = some x.