@[inline]

def Auto.Option.allp {α : Type u_1} (p : α → Prop) : Option α → Prop

Equations

• Auto.Option.allp p (some a) = p a
• Auto.Option.allp p none = True

theorem Auto.Option.all_allp {α : Type u_1} (p : α → Bool) (x : Option α) : (Option.all p x = true) = allp (fun (x : α) => p x = true) x

theorem Auto.Option.allp_uniform {α : Type u_1} (p : α → Prop) (x : Option α) : (∀ (x : α), p x) → allp p x

theorem Auto.Option.isNone_eq_not_isSome {α : Type u_1} {x : Option α} : x.isNone = !x.isSome

theorem Auto.Option.isSome_eq_not_isNone {α : Type u_1} {x : Option α} : x.isSome = !x.isNone

theorem Auto.Option.beq_none_none {α : Type u_1} [BEq α] : (none == none) = true

theorem Auto.Option.beq_none_some {α : Type u_1} {x : α} [BEq α] : (none == some x) = false

theorem Auto.Option.beq_some_none {α : Type u_1} {x : α} [BEq α] : (some x == none) = false

theorem Auto.Option.beq_some_some {α : Type u_1} {x y : α} [BEq α] : (some x == some y) = (x == y)

theorem Auto.Option.beq_refl {α : Type u_1} [BEq α] (α_beq_refl : ∀ (x : α), (x == x) = true) {x : Option α} : (x == x) = true

theorem Auto.Option.eq_of_beq_eq_true {α : Type u_1} [BEq α] (α_eq_of_beq_eq_true : ∀ (x y : α), (x == y) = true → x = y) {x y : Option α} (H : (x == y) = true) : x = y