Day 7

1 files changed, 11 insertions, 0 deletions

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