From 4749b3ca572618fa1a7cdb17e2abba9b498279ca Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 5 Jan 2025 23:55:54 +0100
Subject: Move AStar into a separte library and use it for Day17-1

---
 Common/Countable.lean | 9 ---------
 1 file changed, 9 deletions(-)
 delete mode 100644 Common/Countable.lean

(limited to 'Common/Countable.lean')

diff --git a/Common/Countable.lean b/Common/Countable.lean
deleted file mode 100644
index e19db99..0000000
--- a/Common/Countable.lean
+++ /dev/null
@@ -1,9 +0,0 @@
-import Common.Finite
-
-class Countable (α : Type u) where
-  enumerate : α → Nat
-  injective {a b : α} : enumerate a = enumerate b → a = b
-
-instance {α : Type u} [Finite α] : Countable α where
-  enumerate := Fin.val ∘ Finite.enumerate
-  injective :=  Finite.injective ∘ Fin.val_inj.mp
-- 
cgit v1.2.3