• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
• inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
• le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
• le_sup_inf : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
• sdiff : α → α → α
• bot : α
• sup_inf_sdiff : ∀ (a b : α), a ⊓ b ⊔ a \ b = a
• inf_inf_sdiff : ∀ (a b : α), a ⊓ b ⊓ a \ b = ⊥

A generalized Boolean algebra is a distributive lattice with ⊥ and a relative complement operation \ (called sdiff, after "set difference") satisfying (a ⊓ b) ⊔ (a \ b) = a and (a ⊓ b) ⊓ (a \ b) = ⊥, i.e. a \ b is the complement of b in a.

This is a generalization of Boolean algebras which applies to finset α for arbitrary (not-necessarily-fintype) α.

• sup : α → α → α
• le : α → α → Prop
• lt : α → α → Prop
• le_refl : ∀ (a : α), a ≤ a
• le_trans : ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c
• lt_iff_le_not_le : (∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a) . "order_laws_tac"
• le_antisymm : ∀ (a b : α), a ≤ b → b ≤ a → a = b
• le_sup_left : ∀ (a b : α), a ≤ a ⊔ b
• le_sup_right : ∀ (a b : α), b ≤ a ⊔ b
• sup_le : ∀ (a b c : α), a ≤ c → b ≤ c → a ⊔ b ≤ c
• inf : α → α → α
• inf_le_left : ∀ (a b : α), a ⊓ b ≤ a
• inf_le_right : ∀ (a b : α), a ⊓ b ≤ b
• le_inf : ∀ (a b c : α), a ≤ b → a ≤ c → a ≤ b ⊓ c
• le_sup_inf : ∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
• compl : α → α
• sdiff : α → α → α
• himp : α → α → α
• top : α
• bot : α
• inf_compl_le_bot : ∀ (x : α), x ⊓ xᶜ ≤ ⊥
• top_le_sup_compl : ∀ (x : α), ⊤ ≤ x ⊔ xᶜ
• le_top : ∀ (a : α), a ≤ ⊤
• bot_le : ∀ (a : α), ⊥ ≤ a
• sdiff_eq : (∀ (x y : α), x \ y = x ⊓ yᶜ) . "obviously"
• himp_eq : (∀ (x y : α), x ⇨ y = y ⊔ xᶜ) . "obviously"

A Boolean algebra is a bounded distributive lattice with a complement operator ᶜ such that x ⊓ xᶜ = ⊥ and x ⊔ xᶜ = ⊤. For convenience, it must also provide a set difference operation \ and a Heyting implication ⇨ satisfying x \ y = x ⊓ yᶜ and x ⇨ y = y ⊔ xᶜ.

This is a generalization of (classical) logic of propositions, or the powerset lattice.

Since bounded_order, order_bot, and order_top are mixins that require has_le to be present at define-time, the extends mechanism does not work with them. Instead, we extend using the underlying has_bot and has_top data typeclasses, and replicate the order axioms of those classes here. A "forgetful" instance back to bounded_order is provided.