Extra definitions on Option

This file defines more operations involving Option α. Lemmas about them are located in other files under Mathlib.Data.Option. Other basic operations on Option are defined in the core library.

def Option.traverse {F : Type u → Type v} [Applicative F] {α : Type u_1} {β : Type u} (f : α → F β) : Option α → F (Option β)

Traverse an object of Option α with a function f : α → F β for an applicative F.

Equations

• Option.traverse f x = match x with | none => pure none | some x => some <$> f x

@[deprecated Option.getDM]

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

Equations

• Option.getDM' x y = do let __do_lift ← x Option.getDM __do_lift y

def Option.elim' {α : Type u_1} {β : Type u_2} (b : β) (f : α → β) : Option α → β

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

Equations

• Option.elim' b f x = match x with | some a => f a | none => b

@[simp]

theorem Option.elim'_none {α : Type u_1} {β : Type u_2} (b : β) (f : α → β) : Option.elim' b f none = b

@[simp]

theorem Option.elim'_some {α : Type u_1} {β : Type u_2} {a : α} (b : β) (f : α → β) : Option.elim' b f (some a) = f a

theorem Option.elim'_eq_elim {α : Type u_3} {β : Type u_4} (b : β) (f : α → β) (a : Option α) : Option.elim' b f a = Option.elim a b f

theorem Option.mem_some_iff {α : Type u_3} {a : α} {b : α} : a ∈ some b ↔ b = a

@[inline]

def Option.decidableEqNone {α : 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 Option.decidableEq. Try to use o.isNone or o.isSome instead.

Equations

• Option.decidableEqNone = decidable_of_decidable_of_iff ⋯

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

Equations

• Option.decidableForallMem x = match x with | none => isTrue ⋯ | some a => if h : p a then isTrue ⋯ else isFalse ⋯

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

Equations

• Option.decidableExistsMem x = match x with | none => isFalse ⋯ | some a => if h : p a then isTrue ⋯ else isFalse ⋯

@[reducible]

def Option.iget {α : Type u_1} [Inhabited α] : Option α → α

Inhabited get function. Returns a if the input is some a, otherwise returns default.

Equations

• Option.iget x = match x with | some x => x | none => default

theorem Option.iget_some {α : Type u_1} [Inhabited α] {a : α} : Option.iget (some a) = a

@[simp]

theorem Option.mem_toList {α : Type u_1} {a : α} {o : Option α} : a ∈ Option.toList o ↔ a ∈ o

instance Option.liftOrGet_isCommutative {α : Type u_1} (f : α → α → α) [Std.Commutative f] : Std.Commutative (Option.liftOrGet f)

Equations

• ⋯ = ⋯

instance Option.liftOrGet_isAssociative {α : Type u_1} (f : α → α → α) [Std.Associative f] : Std.Associative (Option.liftOrGet f)

Equations

• ⋯ = ⋯

instance Option.liftOrGet_isIdempotent {α : Type u_1} (f : α → α → α) [Std.IdempotentOp f] : Std.IdempotentOp (Option.liftOrGet f)

Equations

• ⋯ = ⋯

instance Option.liftOrGet_isId {α : Type u_1} (f : α → α → α) : Std.LawfulIdentity (Option.liftOrGet f) none

Equations

• ⋯ = ⋯

def Lean.LOption.toOption {α : Type u_3} : Lean.LOption α → Option α

Convert undef to none to make an LOption into an Option.

Equations

• Lean.LOption.toOption x = match x with | Lean.LOption.some a => some a | x => none