Skip to content

Commit

Permalink
fix(order/rel_classes): remove looping instance (#8931)
Browse files Browse the repository at this point in the history
This instance causes loop with `is_total_preorder.to_is_total`, and was unused in the library.

Caught by the new linter (#8932).
  • Loading branch information
fpvandoorn committed Aug 31, 2021
1 parent 53f074c commit 6b63c03
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion src/order/rel_classes.lean
Expand Up @@ -65,7 +65,6 @@ instance [preorder α] : is_antisymm α (<) := is_asymm.is_antisymm _
instance [preorder α] : is_antisymm α (>) := is_asymm.is_antisymm _
instance [preorder α] : is_strict_order α (<) := {}
instance [preorder α] : is_strict_order α (>) := {}
instance preorder.is_total_preorder [preorder α] [is_total α (≤)] : is_total_preorder α (≤) := {}
instance [partial_order α] : is_antisymm α (≤) := ⟨@le_antisymm _ _⟩
instance [partial_order α] : is_antisymm α (≥) := is_antisymm.swap _
instance [partial_order α] : is_partial_order α (≤) := {}
Expand Down

0 comments on commit 6b63c03

Please sign in to comment.