instance Option.instDecidableEq {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (Option α✝)

Equations

• Option.instDecidableEq = Option.decEqOption✝

instance Option.instBEq {α✝ : Type u_1} [BEq α✝] : BEq (Option α✝)

Equations

• Option.instBEq = { beq := Option.beqOption✝ }

def Option.getM {m : Type u_1 → Type u_2} {α : Type u_1} [Alternative m] : Option α → m α

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

Equations

• none.getM = failure
• (some a).getM = pure a

@[inline]

def Option.isSome {α : Type u_1} : Option α → Bool

Returns true on some x and false on none.

Equations

• (some val).isSome = true
• none.isSome = false

@[simp]

theorem Option.isSome_none {α : Type u_1} : none.isSome = false

@[simp]

theorem Option.isSome_some {α✝ : Type u_1} {a : α✝} : (some a).isSome = true

@[inline]

def Option.isNone {α : Type u_1} : Option α → Bool

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

Equations

• (some val).isNone = false
• none.isNone = true

@[simp]

theorem Option.isNone_none {α : Type u_1} : none.isNone = true

@[simp]

theorem Option.isNone_some {α✝ : Type u_1} {a : α✝} : (some a).isNone = false

@[inline]

def Option.isEqSome {α : Type u_1} [BEq α] : Option α → α → Bool

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.

Equations

• (some a).isEqSome x✝ = (a == x✝)
• none.isEqSome x✝ = false

@[inline]

def Option.bind {α : Type u_1} {β : Type u_2} : Option α → (α → Option β) → Option β

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.

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

Equations

• none.bind x✝ = none
• (some a).bind x✝ = x✝ a

@[inline]

def Option.bindM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m (Option β)) (o : Option α) : m (Option β)

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.

Equations

• Option.bindM f (some a) = do let __do_lift ← f a pure __do_lift
• Option.bindM f o = pure none

@[inline]

def Option.mapM {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) (o : Option α) : m (Option β)

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.

Equations

• Option.mapM f (some a) = do let __do_lift ← f a pure (some __do_lift)
• Option.mapM f o = pure none

theorem Option.map_id {α : Type u_1} : Option.map id = id

@[inline]

def Option.filter {α : Type u_1} (p : α → Bool) : Option α → Option α

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

Equations

• Option.filter p (some val) = if p val = true then some val else none
• Option.filter p none = none

@[inline]

def Option.all {α : Type u_1} (p : α → Bool) : Option α → Bool

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

Equations

• Option.all p (some val) = p val
• Option.all p none = true

@[inline]

def Option.any {α : Type u_1} (p : α → Bool) : Option α → Bool

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

Equations

• Option.any p (some val) = p val
• Option.any p none = false

@[macro_inline]

def Option.orElse {α : Type u_1} : Option α → (Unit → Option α) → Option α

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✝ ()

instance Option.instOrElse {α : Type u_1} : OrElse (Option α)

Equations

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

@[macro_inline]

def Option.or {α : Type u_1} : Option α → Option α → Option α

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.

Equations

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

@[inline]

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

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

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

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

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

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

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

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)

@[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 : α → Option β) : none.bind f = none

@[simp]

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

@[inline]

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

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

Equations

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

@[inline]

def Option.get {α : Type u} (o : Option α) : o.isSome = true → α

Extracts the value from an option that can be proven to be some.

Equations

• (some x_2).get x_3 = x_2

@[simp]

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

@[simp]

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

@[inline]

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

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

Equations

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

@[inline]

def Option.toList {α : Type u_1} : Option α → List α

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

Examples:

• (some "value").toList = ["value"]
• none.toList = []

Equations

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

@[inline]

def Option.toArray {α : Type u_1} : Option α → Array α

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

Examples:

• (some "value").toArray = #["value"]
• none.toArray = #[]

Equations

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

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

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

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)

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

@[inline]

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

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

Equations

• x.join = x.bind id

@[inline]

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

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.

Equations

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

@[inline]

def Option.sequence {m : Type u → Type u_1} [Monad m] {α : Type u} : Option (m α) → m (Option α)

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

Example:

#eval show IO (Option String) from
  Option.sequence <| some do
    IO.println "hello"
    return "world"

hello

some "world"

Equations

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

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

Equations

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

@[inline]

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

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

This is the monadic analogue of Option.getD.

Equations

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

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

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

@[simp]

theorem Option.any_none {α✝ : Type u_1} {p : α✝ → Bool} : Option.any p none = false

@[simp]

theorem Option.any_some {α✝ : Type u_1} {p : α✝ → Bool} {x : α✝} : Option.any p (some x) = p x

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

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

Equations

• (some x_2).min (some y) = some (min x_2 y)
• (some val).min none = none
• none.min (some val) = none
• none.min none = none

instance Option.instMin {α : Type u_1} [Min α] : Min (Option α)

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 = none

@[simp]

theorem Option.min_none_some {α : Type u_1} [Min α] {b : α} : min none (some b) = none

@[simp]

theorem Option.min_none_none {α : Type u_1} [Min α] : min none none = none

def Option.max {α : Type u_1} [Max α] : Option α → Option α → Option α

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

Equations

• (some x_2).max (some y) = some (max x_2 y)
• (some val).max none = some val
• none.max (some val) = some val
• none.max none = none

instance Option.instMax {α : Type u_1} [Max α] : Max (Option α)

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 (Option α)

Equations

• instLTOption = { lt := Option.lt fun (x1 x2 : α) => x1 < x2 }

instance instLEOption {α : Type u_1} [LE α] : LE (Option α)

Equations

• instLEOption = { le := Option.le fun (x1 x2 : α) => x1 ≤ x2 }

@[always_inline]

instance instFunctorOption : Functor Option

Equations

• instFunctorOption = { map := fun {α β : Type ?u.9} => Option.map }

@[always_inline]

instance instMonadOption : Monad Option

Equations

• One or more equations did not get rendered due to their size.

@[always_inline]

instance instAlternativeOption : Alternative Option

Equations

• instAlternativeOption = { toApplicative := Monad.toApplicative, failure := fun {α : Type ?u.5} => none, orElse := fun {α : Type ?u.5} => Option.orElse }

def liftOption {m : Type u_1 → Type u_2} {α : Type u_1} [Alternative m] : Option α → m α

Equations

• liftOption (some val) = pure val
• liftOption none = failure

@[inline]

def Option.tryCatch {α : Type u_1} (x : Option α) (handle : Unit → Option α) : Option α

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"

Equations

• (some val).tryCatch handle = some val
• none.tryCatch handle = handle ()

instance instMonadExceptOfUnitOption : MonadExceptOf Unit Option

Equations

• instMonadExceptOfUnitOption = { throw := fun {α : Type ?u.6} (x : Unit) => none, tryCatch := fun {α : Type ?u.6} => Option.tryCatch }