fix(conditionally_complete_lattice): add instance (#4183)

there was no instance from `conditionally_complete_linear_order_bot` to `conditionally_complete_linear_order`. It is added by this change.
leanprover-community · Sep 18, 2020 · bf7a2ed · bf7a2ed
1 parent c2ae6c0
commit bf7a2ed
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/order/conditionally_complete_lattice.lean b/src/order/conditionally_complete_lattice.lean
@@ -74,7 +74,7 @@ class conditionally_complete_linear_order (α : Type*)
   extends conditionally_complete_lattice α, decidable_linear_order α
 
 class conditionally_complete_linear_order_bot (α : Type*)
-  extends conditionally_complete_lattice α, decidable_linear_order α, order_bot α :=
+  extends conditionally_complete_linear_order α, order_bot α :=
 (cSup_empty : Sup ∅ = ⊥)
 
 /- A complete lattice is a conditionally complete lattice, as there are no restrictions