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

• Option.elim x✝¹ x✝ x = match x✝¹, x✝, x with | some x, x_1, f => f x | none, y, x => y

instance Option.instMembershipOption {α : Type u_1} : Membership α (Option α)

Equations

• Option.instMembershipOption = { mem := fun (a : α) (b : Option α) => b = some a }

@[simp]

theorem Option.mem_def {α : Type u_1} {a : α} {b : Option α} : a ∈ b ↔ b = some a

instance Option.instDecidableMemOptionInstMembershipOption {α : Type u_1} [DecidableEq α] (j : α) (o : Option α) : Decidable (j ∈ o)

Equations

• Option.instDecidableMemOptionInstMembershipOption j o = inferInstanceAs (Decidable (o = some j))

theorem Option.isNone_iff_eq_none {α : Type u_1} {o : Option α} : Option.isNone o = true ↔ o = none

theorem Option.some_inj {α : Type u_1} {a : α} {b : α} : some a = some b ↔ a = b

@[inline]

def Option.decidable_eq_none {α : Type u_1} {o : Option α} : Decidable (o = none)

o = none is decidable even if the wrapped type does not have decidable equality. This is not an instance because it is not definitionally equal to instance : DecidableEq Option. Try to use o.isNone or o.isSome instead.

Equations

• Option.decidable_eq_none = decidable_of_decidable_of_iff (_ : Option.isNone o = true ↔ o = none)

instance Option.instForAllOptionDecidableForAllMemInstMembershipOption {α : Type u_1} {p : α → Prop} [DecidablePred p] (o : Option α) : Decidable (∀ (a : α), a ∈ o → p a)

Equations

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

instance Option.instForAllOptionDecidableExistsAndMemInstMembershipOption {α : Type u_1} {p : α → Prop} [DecidablePred p] (o : Option α) : Decidable (∃ (a : α), a ∈ o ∧ p a)

Equations

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

@[inline]

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

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

Equations

• Option.get x✝ x = match x✝, x with | some x, x_1 => 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

• Option.toList x = match x with | none => [] | some a => [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

• Option.toArray x = match x with | none => #[] | some a => #[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 x✝ x = match x✝, x with | none, none => none | some a, none => some a | none, some b => some b | some a, some b => some (f a b)

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 → Option.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

@[inline]

def Option.pbind {α : Type u_1} {β : Type u_2} (x : Option α) : ((a : α) → a ∈ x → Option β) → Option β

Partial bind. If for some x : Option α, f : Π (a : α), a ∈ x → Option β is a partial function defined on a : α giving an Option β, where some a = x, then pbind x f h is essentially the same as bind x f but is defined only when all x = some a, using the proof to apply f.

Equations

• Option.pbind x✝ x = match x✝, x with | none, x => none | some a, f => f a (_ : some a = some a)

@[inline]

def Option.pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (x : Option α) : (∀ (a : α), a ∈ x → p a) → Option β

Partial map. If f : Π a, p a → β is a partial function defined on a : α satisfying p, then pmap f x h is essentially the same as map f x but is defined only when all members of x satisfy p, using the proof to apply f.

Equations

• Option.pmap f x✝ x = match x✝, x with | none, x => none | some a, H => some (f a (_ : p a))

@[inline]

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

Flatten an Option of Option, a specialization of joinM.

Equations

• Option.join x = Option.bind x id

@[inline]

def Option.forM {m : Type → Type u_1} {α : Type u_2} [Pure m] : Option α → (α → m PUnit) → m PUnit

Map a monadic function which returns Unit over an Option.

Equations

• Option.forM x✝ x = match x✝, x with | none, x => pure () | some a, f => f a

instance Option.instForMOption {m : Type → Type u_1} {α : Type u_2} : ForM m (Option α) α

Equations

• Option.instForMOption = { forM := fun [Monad m] => Option.forM }

instance Option.instForIn'OptionInferInstanceMembershipInstMembershipOption {m : Type u_1 → Type u_2} {α : Type u_3} : ForIn' m (Option α) α inferInstance

Equations

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

@[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 x = match x with | none => pure none | some x => some <$> f x

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

• Option.sequence x = match x with | none => pure none | some fn => some <$> fn

@[inline]

def Option.elimM {m : Type u_1 → Type u_2} {α : Type u_1} {β : 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 Option.elim __do_lift 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

• Option.getDM x y = match x with | some a => pure a | none => y

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

Equations

• (_ : LawfulBEq (Option α)) = (_ : 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

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

The minimum of two optional values.

Equations

• Option.min x✝ x = match x✝, x with | some x, some y => some (min x y) | some x, none => some x | none, some y => some y | none, none => none

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

Equations

• Option.instMinOption = { 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

• Option.max x✝ x = match x✝, x with | some x, some y => some (max x y) | some x, none => some x | none, some y => some y | none, none => none

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

Equations

• Option.instMaxOption = { 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