From 5e75e251e5652908e23b4977e98600688ff9fd81 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Fri, 8 Dec 2023 15:15:33 +0100
Subject: Day 7

---
 Common/Helpers.lean | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'Common/Helpers.lean')

diff --git a/Common/Helpers.lean b/Common/Helpers.lean
index f57f826..593f7c5 100644
--- a/Common/Helpers.lean
+++ b/Common/Helpers.lean
@@ -1,2 +1,13 @@
 def curry (g : (α × β) → γ) : α → β → γ := λ a b ↦ g (a,b)
 def uncurry (f : α → β → γ) : (α × β) → γ := λ (a,b) ↦ f a b
+
+-- Default instance for LT, LE for anything that's Ord.
+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
+    Decidable.isTrue p
+  else
+    Decidable.isFalse p
-- 
cgit v1.2.3