From f7ac27f54a76582354964bae21ee03937c108187 Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Fri, 12 Jul 2024 22:01:57 +0200 Subject: Squashed commit of the following: commit 7aeefe2e761a4892ff2f438e00f3ec7e6d286c5c Author: Andreas Grois Date: Fri Jul 12 21:59:44 2024 +0200 Finish Lean 4.9 update. commit 8a5576ae983203035f6bf0c807b36f1b4d7b63a6 Author: Andreas Grois Date: Fri Jul 12 21:40:21 2024 +0200 Lean 4.9 upgrade, heap is where it was before... commit db34881e21391c96a6a0b939552b0f6f77d05bd8 Author: Andreas Grois Date: Fri Jul 12 00:31:22 2024 +0200 Further Lean 4.9 compat... commit 22444613d58c5bd1a3fcdad0cd6c8d3aee1f3214 Author: Andreas Grois Date: Thu Jul 11 22:15:11 2024 +0200 Further Lean 4.9 porting commit a4ace32cbb02959f9625578b511c2486e0816367 Author: Andreas Grois Date: Wed Jul 10 23:18:29 2024 +0200 Continue porting to Lean 4.9 commit d0f411bcc42b5cb7c72c2ed65ae35875c72e95dd Author: Andreas Grois Date: Wed Jul 10 23:10:34 2024 +0200 Continue port to Lean 4.9 commit 835ce644b97840048de0df40676ff6f3a8b99985 Author: Andreas Grois Date: Wed Jul 10 22:14:59 2024 +0200 Partial port to Lean 4.9. Not compiling yet. --- Common/Helpers.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Common/Helpers.lean') 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 -- cgit v1.2.3