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 +++++++++++
 Common/List.lean    | 14 ++++++++++++++
 Common/String.lean  |  2 ++
 3 files changed, 27 insertions(+)

(limited to 'Common')

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
diff --git a/Common/List.lean b/Common/List.lean
index 1d770a8..5d82e89 100644
--- a/Common/List.lean
+++ b/Common/List.lean
@@ -48,3 +48,17 @@ def dedup {α : Type} [BEq α] (input : List α) : List α :=
   match input with
   | [] => []
   | a :: as => a :: helper as a
+
+def compare {α : Type} [Ord α] (a b : List α) := match a, b with
+  | _ :: _, [] => Ordering.gt
+  | [], _ :: _ => Ordering.lt
+  | [], [] => Ordering.eq
+  | a :: as, b :: bs =>
+    let ab := Ord.compare a b
+    if ab != Ordering.eq then
+      ab
+    else
+      compare as bs
+
+instance {α : Type} [Ord α] : Ord (List α) where
+  compare := compare
diff --git a/Common/String.lean b/Common/String.lean
index 7fe7aee..3edbd63 100644
--- a/Common/String.lean
+++ b/Common/String.lean
@@ -2,3 +2,5 @@ namespace String
 
 def splitTrim (c : Char → Bool) (s : String) : List String :=
   String.trim <$> s.split c
+
+def notEmpty : String → Bool := not ∘ isEmpty
-- 
cgit v1.2.3