Init.Data.Option.Basic

Option.instDecidableEq instance

{α✝} [DecidableEq✝ α✝] : DecidableEq✝ (@Option✝ α✝)

Full source

DecidableEq for Option

Decidable Equality for Optional Values

Informal description

For any type $\alpha$ with decidable equality, the type `Option α` of optional values also has decidable equality.

Option.instBEq instance

{α✝} [BEq✝ α✝] : BEq✝ (@Option✝ α✝)

Full source

BEq for Option

Boolean Equality for Optional Values

Informal description

For any type $\alpha$ equipped with a boolean equality relation `==`, the type `Option α` of optional values also has a boolean equality relation defined as follows: `none == none` is `true`, `some x == some y` is `x == y`, and all other cases are `false`.

Option.getM definition

[Alternative m] : Option α → m α

Full source

/-- Lifts an optional value to any `Alternative`, sending `none` to `failure`. -/
def getM [Alternative m] : Option α → m α
  | none     => failure
  | some a   => pure a

Lifting optional values to an Alternative type

Informal description

The function `Option.getM` lifts an optional value of type `Option α` to any `Alternative` type `m α`, where `none` is mapped to `failure` and `some a` is mapped to `pure a`.

Option.isSome definition

: Option α → Bool

Full source

/-- Returns `true` on `some x` and `false` on `none`. -/
@[inline] def isSome : Option α → Bool
  | some _ => true
  | none   => false

Check if an optional value is `some`

Informal description

The function `Option.isSome` takes an optional value of type `Option α` and returns `true` if it is of the form `some x` and `false` if it is `none`.

Option.isSome_none theorem

: @isSome α none = false

Full source

@[simp] theorem isSome_none : @isSome α none = false := rfl

`isSome none` is false

Informal description

For any type $\alpha$, the function `isSome` applied to the optional value `none` returns `false$.

Option.isSome_some theorem

: isSome (some a) = true

Full source

@[simp] theorem isSome_some : isSome (some a) = true := rfl

`isSome` returns true for `some` values

Informal description

For any element $a$ of type $\alpha$, the function `isSome` applied to the optional value `some a` returns `true`.

Option.isNone definition

: Option α → Bool

Full source

/--
Returns `true` on `none` and `false` on `some x`.

This function is more flexible than `(· == none)` because it does not require a `BEq α` instance.

Examples:
 * `(none : Option Nat).isNone = true`
 * `(some Nat.add).isNone = false`
-/
@[inline] def isNone : Option α → Bool
  | some _ => false
  | none   => true

Check if an optional value is none

Informal description

The function `isNone` takes an optional value of type `Option α` and returns `true` if the value is `none`, and `false` if it is `some x` for some `x : α`.

Option.isNone_none theorem

: @isNone α none = true

Full source

@[simp] theorem isNone_none : @isNone α none = true := rfl

`isNone` returns true for `none`

Informal description

For any type $\alpha$, the function `isNone` applied to the optional value `none` returns `true`.

Option.isNone_some theorem

: isNone (some a) = false

Full source

@[simp] theorem isNone_some : isNone (some a) = false := rfl

`isNone` returns false for `some a`

Informal description

For any element $a$ of type $\alpha$, the function `isNone` evaluates to `false` when applied to the optional value `some a`.

Option.isEqSome definition

[BEq α] : Option α → α → Bool

Full source

/--
Checks whether an optional value is both present and equal to some other value.

Given `x? : Option α` and `y : α`, `x?.isEqSome y` is equivalent to `x? == some y`. It is more
efficient because it avoids an allocation.
-/
@[inline] def isEqSome [BEq α] : Option α → α → Bool
  | some a, b => a == b
  | none,   _ => false

Check if optional value equals given value

Informal description

Given an optional value `x? : Option α` and a value `y : α`, the function `Option.isEqSome` checks whether `x?` is `some y` (i.e., whether `x?` is present and equal to `y`). This is equivalent to `x? == some y` but avoids an allocation, making it more efficient.

Option.bind definition

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

Full source

/--
Sequencing of `Option` computations.

From the perspective of `Option` as computations that might fail, this function sequences
potentially-failing computations, failing if either fails. From the perspective of `Option` as a
collection with at most one element, the function is applied to the element if present, and the
final result is empty if either the initial or the resulting collections are empty.

This function is often accessed via the `>>=` operator from the `Bind (Option α)` instance, or
implicitly via `do`-notation, but it is also idiomatic to call it using [generalized field
notation](lean-manual://section/generalized-field-notation).

Examples:
 * `none.bind (fun x => some x) = none`
 * `(some 4).bind (fun x => some x) = some 4`
 * `none.bind (Option.guard (· > 2)) = none`
 * `(some 2).bind (Option.guard (· > 2)) = none`
 * `(some 4).bind (Option.guard (· > 2)) = some 4`
-/
@[inline] protected def bind : Option α → (α → Option β) → Option β
  | none,   _ => none
  | some a, f => f a

Sequential composition of optional computations

Informal description

The function `Option.bind` takes an optional value of type `α` and a function from `α` to an optional value of type `β`, and returns an optional value of type `β`. If the input is `none`, the result is `none`. If the input is `some a`, the result is obtained by applying the function to `a`. This operation sequences potentially-failing computations (where `none` represents failure), failing if either the input or the function application fails. It can also be viewed as applying a function to the element of a collection with at most one element, resulting in an empty collection if either the input or the output is empty.

Option.bindM definition

[Monad m] (f : α → m (Option β)) (o : Option α) : m (Option β)

Full source

/--
Runs the monadic action `f` on `o`'s value, if any, and returns the result, or  `none` if there is
no value.

From the perspective of `Option` as a collection with at most one element, the monadic the function
is applied to the element if present, and the final result is empty if either the initial or the
resulting collections are empty.
-/
@[inline] protected def bindM [Monad m] (f : α → m (Option β)) (o : Option α) : m (Option β) := do
  if let some a := o then
    return (← f a)
  else
    return none

Monadic bind for optional values

Informal description

Given a monadic function $f : \alpha \to m (\text{Option } \beta)$ and an optional value $o : \text{Option } \alpha$, the function `Option.bindM` applies $f$ to the value inside $o$ if it exists (i.e., if $o = \text{some } a$), returning the result. If $o = \text{none}$, it returns $\text{none}$ without invoking $f$. This operation sequences monadic computations that may fail (represented by $\text{none}$), failing if either the input or the function application fails.

Option.mapM definition

[Monad m] (f : α → m β) (o : Option α) : m (Option β)

Full source

/--
Runs a monadic function `f` on an optional value, returning the result. If the optional value is
`none`, the function is not called and the result is also `none`.

From the perspective of `Option` as a container with at most one element, this is analogous to
`List.mapM`, returning the result of running the monadic function on all elements of the container.

`Option.mapA` is the corresponding operation for applicative functors.
-/
@[inline] protected def mapM [Monad m] (f : α → m β) (o : Option α) : m (Option β) := do
  if let some a := o then
    return some (← f a)
  else
    return none

Monadic mapping over optional values

Informal description

Given a monadic function $f : \alpha \to m \beta$ and an optional value $o : \text{Option } \alpha$, the function `Option.mapM` applies $f$ to the value inside $o$ if it exists (i.e., if $o = \text{some } a$), returning the result wrapped in $\text{some}$. If $o = \text{none}$, it returns $\text{none}$ without invoking $f$. This operation generalizes `List.mapM` to optional values, treating them as containers with at most one element.

Option.map_id theorem

: (Option.map id : Option α → Option α) = id

Full source

theorem map_id : (Option.map id : Option α → Option α) = id :=
  funext (fun o => match o with | none => rfl | some _ => rfl)

Identity Mapping Law for Optional Values: $\text{Option.map id} = \text{id}$

Informal description

For any type $\alpha$, the function `Option.map` applied to the identity function `id` is equal to the identity function on `Option α`. That is, $\text{Option.map id} = \text{id}$ as functions from $\text{Option } \alpha$ to $\text{Option } \alpha$.

Option.filter definition

(p : α → Bool) : Option α → Option α

Full source

/--
Keeps an optional value only if it satisfies a Boolean predicate.

If `Option` is thought of as a collection that contains at most one element, then `Option.filter` is
analogous to `List.filter` or `Array.filter`.

Examples:
 * `(some 5).filter (· % 2 == 0) = none`
 * `(some 4).filter (· % 2 == 0) = some 4`
 * `none.filter (fun x : Nat => x % 2 == 0) = none`
 * `none.filter (fun x : Nat => true) = none`
-/
@[always_inline, inline] protected def filter (p : α → Bool) : Option α → Option α
  | some a => if p a then some a else none
  | none   => none

Filtering optional values by a predicate

Informal description

Given a predicate $p : \alpha \to \text{Bool}$ and an optional value $o : \text{Option } \alpha$, the function `Option.filter` returns `some a` if $o = \text{some } a$ and $p(a) = \text{true}$, and returns `none` otherwise. In other words, it retains the value inside the optional if it satisfies the predicate, and discards it otherwise.

Option.all definition

(p : α → Bool) : Option α → Bool

Full source

/--
Checks whether an optional value either satisfies a Boolean predicate or is `none`.

Examples:
 * `(some 33).all (· % 2 == 0) = false
 * `(some 22).all (· % 2 == 0) = true
 * `none.all (fun x : Nat => x % 2 == 0) = true
-/
@[always_inline, inline] protected def all (p : α → Bool) : Option α → Bool
  | some a => p a
  | none   => true

Universal quantification over optional values

Informal description

Given a predicate $ p : \alpha \to \text{Bool} $ and an optional value $ o : \text{Option} \alpha $, the function returns `true` if either $ o $ is `none` or the predicate $ p $ holds for the value contained in $ o $.

Option.any definition

(p : α → Bool) : Option α → Bool

Full source

/--
Checks whether an optional value is not `none` and satisfies a Boolean predicate.

Examples:
 * `(some 33).any (· % 2 == 0) = false
 * `(some 22).any (· % 2 == 0) = true
 * `none.any (fun x : Nat => true) = false
-/
@[always_inline, inline] protected def any (p : α → Bool) : Option α → Bool
  | some a => p a
  | none   => false

Existential quantification over optional values

Informal description

Given a predicate $ p : \alpha \to \text{Bool} $ and an optional value $ o : \text{Option} \alpha $, the function returns `true` if $ o $ is `some a` and the predicate $ p(a) $ holds, and `false` otherwise.

Option.orElse definition

: Option α → (Unit → Option α) → Option α

Full source

/--
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.
-/
@[always_inline, macro_inline] protected def orElse : Option α → (Unit → Option α) → Option α
  | some a, _ => some a
  | none,   b => b ()

Short-circuiting choice for optional values

Informal description

The function takes an optional value `o : Option α` and a function `f : Unit → Option α`. If `o` is `some a`, it returns `some a`. Otherwise, it evaluates and returns the result of `f ()`. This implements the `<|>` syntax for `Option`, providing a short-circuiting behavior where the second argument is only evaluated if the first is `none`.

Option.instOrElse instance

: OrElse (Option α)

Full source

instance : OrElse (Option α) where
  orElse := Option.orElse

The "Or Else" Operation on Optional Values

Informal description

The type `Option α` of optional values can be equipped with an "or else" operation that returns the first non-empty value, or the second value if the first is empty. Specifically, given `x : Option α` and a lazy computation `y : Unit → Option α`, the operation returns `x` if it is `some a`, otherwise it evaluates and returns `y ()`.

Option.or definition

: Option α → Option α → Option α

Full source

/--
Returns the first of its arguments that is `some`, or `none` if neither is `some`.

This is similar to the `<|>` operator, also known as `OrElse.orElse`, but both arguments are always
evaluated without short-circuiting.
-/
@[always_inline, macro_inline] def or : Option α → Option α → Option α
  | some a, _ => some a
  | none,   b => b

Non-short-circuiting choice between optional values

Informal description

The function takes two optional values of type `α` and returns the first one that is `some`, or `none` if both are `none`. Unlike the short-circuiting `<|>` operator, this function evaluates both arguments fully before returning a result.

Option.lt definition

(r : α → β → Prop) : Option α → Option β → Prop

Full source

/--
Lifts an ordering relation to `Option`, such that `none` is the least element.

It can be understood as adding a distinguished least element, represented by `none`, to both `α` and
`β`.

This definition is part of the implementation of the `LT (Option α)` instance. However, because it
can be used with heterogeneous relations, it is sometimes useful on its own.

Examples:
 * `Option.lt (fun n k : Nat => n < k) none none = False`
 * `Option.lt (fun n k : Nat => n < k) none (some 3) = True`
 * `Option.lt (fun n k : Nat => n < k) (some 3) none = False`
 * `Option.lt (fun n k : Nat => n < k) (some 4) (some 5) = True`
 * `Option.lt (fun n k : Nat => n < k) (some 4) (some 4) = False`
-/
@[inline] protected def lt (r : α → β → Prop) : Option α → Option β → Prop
  | none,   some _ => True
  | some x, some y => r x y
  | _,      _      => False

Lifted ordering relation on optional values

Informal description

Given a relation $r : \alpha \to \beta \to \text{Prop}$, the function $\text{Option.lt}$ lifts $r$ to a relation on $\text{Option}\ \alpha$ and $\text{Option}\ \beta$ such that: - $\text{none}$ is less than any $\text{some}\ y$ (returns $\text{True}$) - $\text{some}\ x$ is less than $\text{some}\ y$ if and only if $r\ x\ y$ holds - All other cases return $\text{False}$ This effectively adds a distinguished least element ($\text{none}$) to both types when viewed through the relation $r$.

Option.le definition

(r : α → β → Prop) : Option α → Option β → Prop

Full source

@[inline] protected def le (r : α → β → Prop) : Option α → Option β → Prop
  | none,   some _ => True
  | none,   none   => True
  | some _, none   => False
  | some x, some y => r x y

Lifting a relation to optional values

Informal description

The relation `Option.le r` is defined on optional values of types `α` and `β` with respect to a given relation `r : α → β → Prop`. For two optional values `x : Option α` and `y : Option β`, the relation holds in the following cases: 1. If `x` is `none` and `y` is any value (including `none`), the relation holds (returns `True`). 2. If `x` is `some a` and `y` is `none`, the relation does not hold (returns `False`). 3. If both `x` and `y` are `some` values, the relation holds if and only if `r a b` holds for the underlying values `a` and `b`.

Option.instDecidableRelLt instance

(r : α → β → Prop) [s : DecidableRel r] : DecidableRel (Option.lt r)

Full source

instance (r : α → β → Prop) [s : DecidableRel r] : DecidableRel (Option.lt r)
  | none,   some _ => isTrue  trivial
  | some x, some y => s x y
  | some _, none   => isFalse not_false
  | none,   none   => isFalse not_false

Decidability of the Lifted Ordering Relation on Optional Values

Informal description

For any relation $r : \alpha \to \beta \to \mathrm{Prop}$ that is decidable, the lifted relation $\mathrm{Option.lt}\ r$ on optional values is also decidable. Here, $\mathrm{Option.lt}\ r$ is defined such that: - $\mathrm{none}$ is considered less than any $\mathrm{some}\ y$, - $\mathrm{some}\ x$ is less than $\mathrm{some}\ y$ if and only if $r\ x\ y$ holds, - and all other cases are not less than.

Option.merge definition

(fn : α → α → α) : Option α → Option α → Option α

Full source

/--
Applies a function to a two optional values if both are present. Otherwise, if one value is present,
it is returned and the function is not used.

The value is `some (fn a b)` if the inputs are `some a` and `some b`. Otherwise, the behavior is
equivalent to `Option.orElse`: if only one input is `some x`, then the value is `some x`, and if
both are `none`, then the value is `none`.

Examples:
 * `Option.merge (· + ·) none (some 3) = some 3`
 * `Option.merge (· + ·) (some 2) (some 3) = some 5`
 * `Option.merge (· + ·) (some 2) none = some 2`
 * `Option.merge (· + ·) none none = none`
-/
def merge (fn : α → α → α) : Option α → Option α → Option α
  | none  , none   => none
  | some x, none   => some x
  | none  , some y => some y
  | some x, some y => some <| fn x y

Merging optional values with a binary function

Informal description

Given a binary function $f : \alpha \to \alpha \to \alpha$ and two optional values of type $\alpha$, the function `Option.merge` applies $f$ to the values if both are present (i.e., `some x` and `some y`), returning `some (f x y)`. If only one value is present, it returns that value. If neither value is present, it returns `none`.

Option.getD_none theorem

: getD none a = a

Full source

@[simp] theorem getD_none : getD none a = a := rfl

Default Value for `none` in Optional Type

Informal description

For any element $a$ of type $\alpha$, the function `getD` applied to `none` and $a$ returns $a$, i.e., $\text{getD}(\text{none}, a) = a$.

Option.getD_some theorem

: getD (some a) b = a

Full source

@[simp] theorem getD_some : getD (some a) b = a := rfl

Default Value Extraction from `some` in Optional Type

Informal description

For any elements $a$ and $b$ of type $\alpha$, the function `getD` applied to `some a` and $b$ returns $a$, i.e., $\text{getD}(\text{some } a, b) = a$.

Option.map_none' theorem

(f : α → β) : none.map f = none

Full source

@[simp] theorem map_none' (f : α → β) : none.map f = none := rfl

Mapping over `none` yields `none`

Informal description

For any function $f : \alpha \to \beta$, applying the map operation to the `none` value of type `Option α` yields `none` of type `Option β$, i.e., $\text{map } f \text{ none} = \text{none}$.

Option.map_some' theorem

(a) (f : α → β) : (some a).map f = some (f a)

Full source

@[simp] theorem map_some' (a) (f : α → β) : (some a).map f = some (f a) := rfl

Mapping Preserves `some` in Optional Types

Informal description

For any element $a$ of type $\alpha$ and any function $f : \alpha \to \beta$, applying the map operation to the optional value $\text{some } a$ yields $\text{some } (f a)$, i.e., $(\text{some } a).\text{map } f = \text{some } (f a)$.

Option.none_bind theorem

(f : α → Option β) : none.bind f = none

Full source

@[simp] theorem none_bind (f : α → Option β) : none.bind f = none := rfl

Binding `none` with any function yields `none`

Informal description

For any function $f : \alpha \to \text{Option } \beta$, binding $f$ to the `none` value of type $\text{Option } \alpha$ yields `none` of type $\text{Option } \beta$, i.e., $\text{none.bind } f = \text{none}$.

Option.some_bind theorem

(a) (f : α → Option β) : (some a).bind f = f a

Full source

@[simp] theorem some_bind (a) (f : α → Option β) : (some a).bind f = f a := rfl

Binding `some a` with $f$ yields $f(a)$

Informal description

For any element $a$ of type $\alpha$ and any function $f : \alpha \to \text{Option } \beta$, binding $f$ to the optional value $\text{some } a$ yields $f(a)$, i.e., $(\text{some } a).\text{bind } f = f(a)$.

Option.elim definition

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

Full source

/--
A case analysis function for `Option`.

Given a value for `none` and a function to apply to the contents of `some`, `Option.elim` checks
which constructor a given `Option` consists of, and uses the appropriate argument.

`Option.elim` is an elimination principle for `Option`. In particular, it is a non-dependent version
of `Option.recOn`. It can also be seen as a combination of `Option.map` and `Option.getD`.

Examples:
 * `(some "hello").elim 0 String.length = 5`
 * `none.elim 0 String.length = 0`
-/
@[inline] protected def elim : Option α → β → (α → β) → β
  | some x, _, f => f x
  | none, y, _ => y

Elimination principle for optional values

Informal description

Given an optional value of type `Option α`, a default value of type `β` for the `none` case, and a function `f : α → β` to apply to the contents of the `some` case, `Option.elim` returns `f x` if the input is `some x`, and returns the default value if the input is `none`.

Option.get definition

{α : Type u} : (o : Option α) → isSome o → α

Full source

/--
Extracts the value from an option that can be proven to be `some`.
-/
@[inline] def get {α : Type u} : (o : Option α) → isSome o → α
  | some x, _ => x

Extraction of value from a non-empty optional type

Informal description

Given an optional value `o : Option α` and a proof that `o` is of the form `some x`, the function returns the value `x` contained in `o`.

Option.some_get theorem

: ∀ {x : Option α} (h : isSome x), some (x.get h) = x

Full source

@[simp] theorem some_get : ∀ {x : Option α} (h : isSome x), some (x.get h) = x
| some _, _ => rfl

Reconstruction of Some Option via Get

Informal description

For any optional value `x : Option α` and a proof `h` that `x` is of the form `some y`, the reconstruction of `x` via `some (x.get h)` equals `x` itself.

Option.get_some theorem

(x : α) (h : isSome (some x)) : (some x).get h = x

Full source

@[simp] theorem get_some (x : α) (h : isSome (some x)) : (some x).get h = x := rfl

Extraction from Some Option Yields Original Value

Informal description

For any element $x$ of type $\alpha$ and a proof $h$ that the optional value $\text{some }x$ is non-empty, extracting the value from $\text{some }x$ using $h$ yields $x$, i.e., $(\text{some }x).\text{get }h = x$.

Option.guard definition

(p : α → Prop) [DecidablePred p] (a : α) : Option α

Full source

/--
Returns `none` if a value doesn't satisfy a predicate, or the value itself otherwise.

From the perspective of `Option` as computations that might fail, this function is a run-time
assertion operator in the `Option` monad.

Examples:
 * `Option.guard (· > 2) 1 = none`
 * `Option.guard (· > 2) 5 = some 5`
-/
@[inline] def guard (p : α → Prop) [DecidablePred p] (a : α) : Option α :=
  if p a then some a else none

Conditional wrapping in `Option` monad

Informal description

Given a predicate $p$ on a type $\alpha$ and an element $a \in \alpha$, the function returns $\text{some }a$ if $p(a)$ holds, and $\text{none}$ otherwise. This can be seen as a runtime assertion in the `Option` monad.

Option.toList definition

: Option α → List α

Full source

/--
Converts an optional value to a list with zero or one element.

Examples:
 * `(some "value").toList = ["value"]`
 * `none.toList = []`
-/
@[inline] def toList : Option α → List α
  | none => .nil
  | some a => .cons a .nil

Conversion from optional value to list

Informal description

The function converts an optional value of type `Option α` to a list of type `List α` containing zero or one element. Specifically, if the input is `none`, the result is the empty list `[]`; if the input is `some a`, the result is the singleton list `[a]`.

Option.toArray definition

: Option α → Array α

Full source

/--
Converts an optional value to an array with zero or one element.

Examples:
 * `(some "value").toArray = #["value"]`
 * `none.toArray = #[]`
-/
@[inline] def toArray : Option α → Array α
  | none => List.toArray .nil
  | some a => List.toArray (.cons a .nil)

Conversion from optional value to array

Informal description

The function converts an optional value of type `Option α` to an array of type `Array α` containing zero or one element. Specifically: - If the input is `none`, the result is the empty array `#[]` - If the input is `some a`, the result is the singleton array `#[a]`

Option.liftOrGet definition

(f : α → α → α) : Option α → Option α → Option α

Full source

/--
Applies a function to a two optional values if both are present. Otherwise, if one value is present,
it is returned and the function is not used.

The value is `some (f a b)` if the inputs are `some a` and `some b`. Otherwise, the behavior is
equivalent to `Option.orElse`. If only one input is `some x`, then the value is `some x`. If both
are `none`, then the value is `none`.

Examples:
 * `Option.liftOrGet (· + ·) none (some 3) = some 3`
 * `Option.liftOrGet (· + ·) (some 2) (some 3) = some 5`
 * `Option.liftOrGet (· + ·) (some 2) none = some 2`
 * `Option.liftOrGet (· + ·) none none = none`
-/
def liftOrGet (f : α → α → α) : Option α → Option α → Option α
  | none, none => none
  | some a, none => some a
  | none, some b => some b
  | some a, some b => some (f a b)

Lifted binary operation on optional values

Informal description

Given a binary function $f : \alpha \to \alpha \to \alpha$ and two optional values $x, y : \text{Option } \alpha$, the function returns: - $\text{some } (f \, a \, b)$ if both $x = \text{some } a$ and $y = \text{some } b$, - $\text{some } a$ if only $x = \text{some } a$ and $y = \text{none}$, - $\text{some } b$ if only $x = \text{none}$ and $y = \text{some } b$, - $\text{none}$ if both $x = \text{none}$ and $y = \text{none}$.

Option.Rel inductive

(r : α → β → Prop) : Option α → Option β → Prop

Full source

/-- Lifts a relation `α → β → Prop` to a relation `Option α → Option β → Prop` by just adding
`none ~ none`. -/
inductive Rel (r : α → β → Prop) : Option α → Option β → Prop
  /-- If `a ~ b`, then `some a ~ some b` -/
  | some {a b} : r a b → Rel r (some a) (some b)
  /-- `none ~ none` -/
  | none : Rel r none none

Lifted relation on optional values

Informal description

Given a relation $r : \alpha \to \beta \to \text{Prop}$, the relation $\text{Option.Rel } r : \text{Option } \alpha \to \text{Option } \beta \to \text{Prop}$ is defined by lifting $r$ to optional values, where $\text{none}$ is only related to $\text{none}$ and $\text{some } x$ is related to $\text{some } y$ if and only if $r \, x \, y$ holds.

Option.join definition

(x : Option (Option α)) : Option α

Full source

/--
Flattens nested optional values, preserving any value found.

This is analogous to `List.flatten`.

Examples:
 * `none.join = none`
 * `(some none).join = none`
 * `(some (some v)).join = some v`
-/
@[simp, inline] def join (x : Option (Option α)) : Option α := x.bind id

Flattening of nested optional values

Informal description

The function flattens a nested optional value of type `Option (Option α)` into a single `Option α`. It preserves any non-`none` value found in the nested structure, analogous to flattening a list of lists. Specifically: - If the input is `none`, the result is `none`. - If the input is `some none`, the result is `none`. - If the input is `some (some v)`, the result is `some v`.

Option.mapA definition

[Applicative m] {α β} (f : α → m β) : Option α → m (Option β)

Full source

/--
Applies a function in some applicative functor to an optional value, returning `none` with no
effects if the value is missing.

This is analogous to `Option.mapM` for monads.
-/
@[inline] protected def mapA [Applicative m] {α β} (f : α → m β) : Option α → m (Option β)
  | none => pure none
  | some x => some <$> f x

Applicative mapping of optional values

Informal description

Given an applicative functor `m`, a function `f : α → m β`, and an optional value `x : Option α`, the function `Option.mapA f x` applies `f` to the value inside `x` if it exists (returning the result wrapped in `some`), or returns `pure none` if `x` is `none`. This operation preserves the applicative effects of `f`.

Option.sequence definition

[Monad m] {α : Type u} : Option (m α) → m (Option α)

Full source

/--
Converts an optional monadic computation into a monadic computation of an optional value.

Example:
```lean example
#eval show IO (Option String) from
  Option.sequence <| some do
    IO.println "hello"
    return "world"
```
```output
hello
```
```output
some "world"
```
-/
@[inline] def sequence [Monad m] {α : Type u} : Option (m α) → m (Option α)
  | none => pure none
  | some fn => some <$> fn

Monadic sequence for optional values

Informal description

Given a monad `m` and an optional monadic computation `x : Option (m α)`, the function `Option.sequence` converts it into a monadic computation `m (Option α)`. If `x` is `none`, it returns `pure none`. If `x` is `some fn`, it applies the monadic computation `fn` and wraps the result in `some`.

Option.elimM definition

[Monad m] (x : m (Option α)) (y : m β) (z : α → m β) : m β

Full source

/--
A monadic case analysis function for `Option`.

Given a fallback computation for `none` and a monadic operation to apply to the contents of `some`,
`Option.elimM` checks which constructor a given `Option` consists of, and uses the appropriate
argument.

`Option.elimM` can also be seen as a combination of `Option.mapM` and `Option.getDM`. It is a
monadic analogue of `Option.elim`.
-/
@[inline] def elimM [Monad m] (x : m (Option α)) (y : m β) (z : α → m β) : m β :=
  do (← x).elim y z

Monadic elimination for optional values

Informal description

Given a monadic computation `x : m (Option α)` producing an optional value, a fallback computation `y : m β` for the `none` case, and a function `z : α → m β` to handle the `some` case, `Option.elimM` performs a monadic case analysis on the result of `x`. If `x` produces `some a`, it applies `z` to `a`; otherwise, it returns the result of `y`. This function combines the functionality of `Option.mapM` and `Option.getDM` in a monadic context.

Option.getDM definition

[Monad m] (x : Option α) (y : m α) : m α

Full source

/--
Gets the value in an option, monadically computing a default value on `none`.

This is the monadic analogue of `Option.getD`.
-/

@[inline] def getDM [Monad m] (x : Option α) (y : m α) : m α :=
  match x with
  | some a => pure a
  | none => y

Monadic default value for optional value

Informal description

Given a monad `m`, an optional value `x : Option α`, and a monadic computation `y : m α`, this function returns the value inside `x` if it is `some a`, otherwise it returns the result of the computation `y`. This is the monadic version of `Option.getD`.

Option.instLawfulBEq instance

(α) [BEq α] [LawfulBEq α] : LawfulBEq (Option α)

Full source

instance (α) [BEq α] [LawfulBEq α] : LawfulBEq (Option α) where
  rfl {x} :=
    match x with
    | some _ => LawfulBEq.rfl (α := α)
    | none => rfl
  eq_of_beq {x y h} := by
    match x, y with
    | some x, some y => rw [LawfulBEq.eq_of_beq (α := α) h]
    | none, none => rfl

Lawful Boolean Equality for Optional Values

Informal description

For any type $\alpha$ with a boolean equality relation `==` that is lawful (i.e., agrees with propositional equality), the type `Option α` of optional values also has a lawful boolean equality relation. Specifically: 1. `none == none` is `true`. 2. For any `x y : α`, `some x == some y` if and only if `x == y`. 3. All other cases (e.g., `none == some _` or `some _ == none`) are `false`.

Option.all_none theorem

: Option.all p none = true

Full source

@[simp] theorem all_none : Option.all p none = true := rfl

Universal Quantification over `none` is True

Informal description

For any predicate $p : \alpha \to \text{Bool}$, the universal quantification over the `none` option evaluates to `true`, i.e., $\text{Option.all}\ p\ \text{none} = \text{true}$.

Option.all_some theorem

: Option.all p (some x) = p x

Full source

@[simp] theorem all_some : Option.all p (some x) = p x := rfl

Universal Quantification over `some x` Equals $p\ x$

Informal description

For any predicate $p : \alpha \to \text{Bool}$ and any element $x : \alpha$, the universal quantification over the option `some x` evaluates to the result of applying $p$ to $x$, i.e., $\text{Option.all}\ p\ (\text{some}\ x) = p\ x$.

Option.any_none theorem

: Option.any p none = false

Full source

@[simp] theorem any_none : Option.any p none = false := rfl

Existential Quantification over `none` is False

Informal description

For any predicate $p : \alpha \to \text{Bool}$, the existential quantification over the `none` option evaluates to `false`, i.e., $\text{Option.any}\ p\ \text{none} = \text{false}$.

Option.any_some theorem

: Option.any p (some x) = p x

Full source

@[simp] theorem any_some : Option.any p (some x) = p x := rfl

Existential Quantification over `some x` Equals $p\ x$

Informal description

For any predicate $p : \alpha \to \text{Bool}$ and any element $x : \alpha$, the existential quantification over the option `some x` evaluates to the result of applying $p$ to $x$, i.e., $\text{Option.any}\ p\ (\text{some}\ x) = p\ x$.

Option.min definition

[Min α] : Option α → Option α → Option α

Full source

/--
The minimum of two optional values, with `none` treated as the least element. This function is
usually accessed through the `Min (Option α)` instance, rather than directly.

Prior to `nightly-2025-02-27`, `none` was treated as the greatest element, so
`min none (some x) = min (some x) none = some x`.

Examples:
 * `Option.min (some 2) (some 5) = some 2`
 * `Option.min (some 5) (some 2) = some 2`
 * `Option.min (some 2) none = none`
 * `Option.min none (some 5) = none`
 * `Option.min none none = none`
-/
protected def min [Min α] : Option α → Option α → Option α
  | some x, some y => some (Min.min x y)
  | some _, none => none
  | none, some _ => none
  | none, none => none

Minimum of optional values (with `none` as least element)

Informal description

The function `Option.min` takes two optional values of type `α` (where `α` has a minimum operation) and returns their minimum, treating `none` as the least element. Specifically: - For `some x` and `some y`, it returns `some (min x y)` - For `some x` and `none`, it returns `none` - For `none` and `some y`, it returns `none` - For `none` and `none`, it returns `none`

Option.instMin instance

[Min α] : Min (Option α)

Full source

instance [Min α] : Min (Option α) where min := Option.min

Minimum Operation on Optional Values

Informal description

For any type $\alpha$ equipped with a minimum operation, the type `Option α` of optional values of $\alpha$ is also equipped with a minimum operation, where `none` is treated as the least element. Specifically: - The minimum of `some x` and `some y` is `some (min x y)` - The minimum of `some x` and `none` is `none` - The minimum of `none` and `some y` is `none` - The minimum of `none` and `none` is `none`

Option.min_some_some theorem

[Min α] {a b : α} : min (some a) (some b) = some (min a b)

Full source

@[simp] theorem min_some_some [Min α] {a b : α} : min (some a) (some b) = some (min a b) := rfl

Minimum of Some Values in Option Type

Informal description

For any type $\alpha$ with a minimum operation and any elements $a, b \in \alpha$, the minimum of the optional values $\text{some } a$ and $\text{some } b$ is equal to $\text{some } (\min(a, b))$.

Option.min_some_none theorem

[Min α] {a : α} : min (some a) none = none

Full source

@[simp] theorem min_some_none [Min α] {a : α} : min (some a) none = none := rfl

Minimum of Some and None is None

Informal description

For any type $\alpha$ with a minimum operation and any element $a \in \alpha$, the minimum of the optional values $\text{some } a$ and $\text{none}$ is equal to $\text{none}$.

Option.min_none_some theorem

[Min α] {b : α} : min none (some b) = none

Full source

@[simp] theorem min_none_some [Min α] {b : α} : min none (some b) = none := rfl

Minimum of None and Some is None

Informal description

For any type $\alpha$ with a minimum operation and any element $b \in \alpha$, the minimum of the optional values $\text{none}$ and $\text{some } b$ is equal to $\text{none}$.

Option.min_none_none theorem

[Min α] : min (none : Option α) none = none

Full source

@[simp] theorem min_none_none [Min α] : min (none : Option α) none = none := rfl

Minimum of Two None Values is None

Informal description

For any type $\alpha$ with a minimum operation, the minimum of two `none` values in `Option α` is `none`.

Option.max definition

[Max α] : Option α → Option α → Option α

Full source

/--
The maximum of two optional values.

This function is usually accessed through the `Max (Option α)` instance, rather than directly.

Examples:
 * `Option.max (some 2) (some 5) = some 5`
 * `Option.max (some 5) (some 2) = some 5`
 * `Option.max (some 2) none = some 2`
 * `Option.max none (some 5) = some 5`
 * `Option.max none none = none`
-/
protected def max [Max α] : Option α → Option α → Option α
  | some x, some y => some (Max.max x y)
  | some x, none => some x
  | none, some y => some y
  | none, none => none

Maximum of two optional values

Informal description

The function that takes two optional values of type `Option α` (where `α` has a maximum operation) and returns their maximum, defined as follows: - If both values are `some x` and `some y`, returns `some (max x y)` - If one value is `some x` and the other is `none`, returns `some x` - If both values are `none`, returns `none`

Option.instMax instance

[Max α] : Max (Option α)

Full source

instance [Max α] : Max (Option α) where max := Option.max

Maximum Operation on Optional Values

Informal description

For any type $\alpha$ equipped with a maximum operation, the type `Option α` of optional values of $\alpha$ can be equipped with a maximum operation defined as follows: - The maximum of `some x` and `some y` is `some (max x y)` - The maximum of `some x` and `none` is `some x` - The maximum of `none` and `none` is `none`

Option.max_some_some theorem

[Max α] {a b : α} : max (some a) (some b) = some (max a b)

Full source

@[simp] theorem max_some_some [Max α] {a b : α} : max (some a) (some b) = some (max a b) := rfl

Maximum of Some Values in Option Type: $\max(\text{some } a, \text{some } b) = \text{some } (\max(a, b))$

Informal description

For any type $\alpha$ equipped with a maximum operation and for any elements $a, b \in \alpha$, the maximum of the optional values $\text{some } a$ and $\text{some } b$ is equal to $\text{some } (\max(a, b))$.

Option.max_some_none theorem

[Max α] {a : α} : max (some a) none = some a

Full source

@[simp] theorem max_some_none [Max α] {a : α} : max (some a) none = some a := rfl

Maximum of Some and None in Option Type: $\max(\text{some } a, \text{none}) = \text{some } a$

Informal description

For any type $\alpha$ equipped with a maximum operation and for any element $a \in \alpha$, the maximum of the optional values $\text{some } a$ and $\text{none}$ is equal to $\text{some } a$.

Option.max_none_some theorem

[Max α] {b : α} : max none (some b) = some b

Full source

@[simp] theorem max_none_some [Max α] {b : α} : max none (some b) = some b := rfl

Maximum of None and Some in Option Type: $\max(\text{none}, \text{some } b) = \text{some } b$

Informal description

For any type $\alpha$ equipped with a maximum operation and for any element $b \in \alpha$, the maximum of the optional values $\text{none}$ and $\text{some } b$ is equal to $\text{some } b$.

Option.max_none_none theorem

[Max α] : max (none : Option α) none = none

Full source

@[simp] theorem max_none_none [Max α] : max (none : Option α) none = none := rfl

Maximum of Two None Options is None

Informal description

For any type $\alpha$ equipped with a maximum operation, the maximum of two `none` values in the option type `Option α` is `none`.

instLTOption instance

[LT α] : LT (Option α)

Full source

instance [LT α] : LT (Option α) where
  lt := Option.lt (· < ·)

The "Less Than" Relation on Optional Values

Informal description

For any type $\alpha$ equipped with a "less than" relation $<$, the type $\text{Option}\ \alpha$ of optional values of $\alpha$ inherits a "less than" relation defined as follows: - $\text{none}$ is less than any $\text{some}\ b$ (where $b \in \alpha$). - For $\text{some}\ a$ and $\text{some}\ b$, $\text{some}\ a < \text{some}\ b$ if and only if $a < b$ in $\alpha$. - All other cases are not less than (return $\text{False}$).

instLEOption instance

[LE α] : LE (Option α)

Full source

instance [LE α] : LE (Option α) where
  le := Option.le (· ≤ ·)

Order on Optional Values

Informal description

For any type $\alpha$ equipped with a "less than or equal to" relation $\leq$, the type `Option α` of optional values of $\alpha$ inherits a "less than or equal to" relation defined as follows: - `none` is less than or equal to any optional value (including `none`). - For `some a` and `some b`, `some a ≤ some b` if and only if $a \leq b$ in $\alpha$. - `some a` is not less than or equal to `none`.

instFunctorOption instance

: Functor Option

Full source

@[always_inline]
instance : Functor Option where
  map := Option.map

The Functor Structure on Optional Values

Informal description

The type constructor `Option` is a functor, meaning it can be mapped over with a function while preserving the structure of optional values. Specifically, for any function `f : α → β`, the functorial action `Option.map f` applies `f` to the value inside an `Option α`, sending `some a` to `some (f a)` and `none` to `none`.

instMonadOption instance

: Monad Option

Full source

@[always_inline]
instance : Monad Option where
  pure := Option.some
  bind := Option.bind

The Monad Structure on Optional Values

Informal description

The type constructor `Option` forms a monad, where the `pure` operation lifts a value `a : α` to `some a`, and the `bind` operation sequences computations by applying a function `f : α → Option β` to the value inside an `Option α`, propagating `none` if either the input or the result of applying `f` is `none`.

instAlternativeOption instance

: Alternative Option

Full source

@[always_inline]
instance : Alternative Option where
  failure := Option.none
  orElse  := Option.orElse

The Alternative Structure on Optional Values

Informal description

The type constructor `Option` forms an alternative functor, providing operations for sequencing computations with optional values, including a choice operation that short-circuits on the first successful computation.

liftOption definition

[Alternative m] : Option α → m α

Full source

def liftOption [Alternative m] : Option α → m α
  | some a => pure a
  | none   => failure

Lifting optional values to an alternative monad

Informal description

Given an alternative monad `m`, the function `liftOption` maps an optional value of type `Option α` to a computation in `m α`. Specifically, it sends `some a` to `pure a` and `none` to `failure`.

Option.tryCatch definition

(x : Option α) (handle : Unit → Option α) : Option α

Full source

/--
Recover from failing `Option` computations with a handler function.

This function is usually accessed through the `MonadExceptOf Unit Option` instance.

Examples:
 * `Option.tryCatch none (fun () => some "handled") = some "handled"`
 * `Option.tryCatch (some "succeeded") (fun () => some "handled") = some "succeeded"`
-/
@[always_inline, inline] protected def Option.tryCatch (x : Option α) (handle : Unit → Option α) : Option α :=
  match x with
  | some _ => x
  | none => handle ()

Recovery from failed optional computation

Informal description

Given an optional value `x : Option α` and a handler function `handle : Unit → Option α`, the function returns `x` if it is `some a`, otherwise it applies the handler to the unit value `()` and returns the result.

instMonadExceptOfUnitOption instance

: MonadExceptOf Unit Option

Full source

instance : MonadExceptOf Unit Option where
  throw    := fun _ => Option.none
  tryCatch := Option.tryCatch

Exception-Handling Monad Structure on Optional Values with Unit Exceptions

Informal description

The type `Option` is a monad that can throw and handle exceptions of type `Unit`.