summaryrefslogtreecommitdiff
path: root/Common/Helpers.lean
diff options
context:
space:
mode:
Diffstat (limited to 'Common/Helpers.lean')
-rw-r--r--Common/Helpers.lean4
1 files changed, 2 insertions, 2 deletions
diff --git a/Common/Helpers.lean b/Common/Helpers.lean
index 593f7c5..fef6f42 100644
--- a/Common/Helpers.lean
+++ b/Common/Helpers.lean
@@ -6,8 +6,8 @@ instance {α : Type} [Ord α]: LT α where
lt := λ a b ↦ Ord.compare a b == Ordering.lt
instance {α : Type} [Ord α]: LE α where
le := λ a b ↦ Ord.compare a b != Ordering.gt
-instance {a b : α} [Ord α] : Decidable (a ≤ b) :=
- if p : Ord.compare a b != Ordering.gt then
+instance {a b : α} [Ord α] : Decidable (a < b) :=
+ if p : Ord.compare a b == Ordering.lt then
Decidable.isTrue p
else
Decidable.isFalse p