1 files changed, 14 insertions, 0 deletions
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