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.

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

x?.isEqSome y is equivalent to x? == some y, but 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 β

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 f on o's value, if any, and returns its result, or else returns none.

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. If the optional value is none the function is not called.

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 the predicate p.

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 that an optional value satisfies a predicate p or is none.

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 that an optional value is not none and the value satisfies a predicate p.

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 α

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✝

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

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 α

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)

@[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 α → β → (α → β) → β

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✝¹

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

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

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

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

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

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)

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 α

Flatten an Option of Option, a specialization of joinM.

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 β)

Like Option.mapM but for applicative functors.

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

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

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

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

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.

Equations

• (some x_2).min (some y) = some (min x_2 y)
• (some x_2).min none = some x_2
• none.min (some y) = some y
• 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 = 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 α] : Option α → Option α → Option α

The maximum of two optional values.

Equations

• (some x_2).max (some y) = some (max x_2 y)
• (some x_2).max none = some x_2
• none.max (some y) = some y
• 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 }

@[always_inline]

instance instFunctorOption : Functor Option

Equations

• instFunctorOption = { map := fun {α β : Type ?u.10} => Option.map, mapConst := fun {α β : Type ?u.10} => Option.map ∘ Function.const β }

@[always_inline]

instance instMonadOption : Monad Option

Equations

• instMonadOption = Monad.mk

@[always_inline]

instance instAlternativeOption : Alternative Option

Equations

• instAlternativeOption = Alternative.mk (fun {α : Type ?u.6} => none) fun {α : Type ?u.6} => 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 α

Equations

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

instance instMonadExceptOfUnitOption : MonadExceptOf Unit Option

Equations

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