Projects.Util.Option

source

def Option.getd {α : Type u_1} [Inhabited α] (x : Option α) :

Equations

none.getd = default
(some x_2).getd = x_2

Instances For

source

@[simp]

theorem Option.failure_bind {α : Type u_1} {β : Type u_2} {f : α → Option β} :

failure.bind f = none

source

@[simp]

theorem Option.exists_eq_some_of_ne_none {α : Type u_1} {x : Option α} (h : x ≠ none) :

∃ (y : α), x = some y

source

@[simp]

theorem Option.guard_bind_eq_some_iff {α : Type u_1} {P : Prop} [Decidable P] {f : Unit → Option α} {x : α} :

(_root_.guard P).bind f = some x ↔ P ∧ f () = some x

source

@[simp]

theorem Option.guard_bind_isSome_iff {α : Type u_1} {P : Prop} [Decidable P] {f : Unit → Option α} :

((_root_.guard P).bind f).isSome = true ↔ P ∧ (f ()).isSome = true

source

@[simp]

theorem Option.get!_with_bot_some {α : Type u_1} [Inhabited α] {x : α} :

get! ↑x = x

source

theorem Option.eq_iff_of_subsingleton {α : Type u_1} [ha : Subsingleton α] {x y : Option α} :

x = y ↔ (x.isSome = true ↔ y.isSome = true)

source

@[simp]

theorem Option.bind_eq_some_iff' {α : Type u_1} {β : Type u_2} {x : Option α} {y : β} {f : α → Option β} :

x.bind f = some y ↔ ∃ (a : α), x = some a ∧ f a = some y

source

theorem Option.bind_dite {α : Type u_1} {β : Type u_2} {P : Prop} [hp : Decidable P] {f : P → Option α} {g : ¬P → Option α} {r : α → Option β} :

(if h : P then f h else g h).bind r = if h : P then (f h).bind r else (g h).bind r

source

theorem Option.bind_ite {α : Type u_1} {β : Type u_2} {P : Prop} [hp : Decidable P] {x y : Option α} {f : α → Option β} :

(if P then x else y).bind f = if P then x.bind f else y.bind f

source

theorem Option.ne_none_of_eq_some {α : Type u_1} {m : Option α} {x : α} (h : m = some x) :

m ≠ none

source

theorem Option.map_elim_fn_some {α : Type u_1} {β : Type u_2} {f : α → β} {x y : Option α} :

Option.map f (x.elim y some) = (Option.map f x).elim (Option.map f y) some

source

@[simp]

theorem Option.elim_init_bool_false_eq_true_iff {α : Type u_1} {m : Option α} {f : α → Bool} :

m.elim false f = true ↔ ∃ (x : α), m = some x ∧ f x = true

source

@[simp]

theorem Option.elim_init_false_iff {α : Type u_1} {m : Option α} {f : α → Prop} :

m.elim False f ↔ ∃ (x : α), m = some x ∧ f x

source

@[simp]

theorem Option.getd_none {α : Type u_1} [ha : Inhabited α] :

none.getd = default

source

@[simp]

theorem Option.getd_some {α : Type u_1} [ha : Inhabited α] {x : α} :

(some x).getd = x

source

theorem Option.getd_eq_getD {α : Type u_1} [ha : Inhabited α] {x : Option α} :

x.getd = x.getD default