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/List.lean | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'Common/List.lean')

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
-- 
cgit v1.2.3