summaryrefslogtreecommitdiff
path: root/Common.lean
diff options
context:
space:
mode:
authorAndreas Grois <andi@grois.info>2024-09-01 00:03:28 +0200
committerAndreas Grois <andi@grois.info>2024-09-01 00:03:28 +0200
commit539545228c4d78cc3fdbf369c3934ad27fd17b32 (patch)
treef59c46671f0bf4ba23159f17bfbcda3026fa3f72 /Common.lean
parent2b6a25a248d7e588cdef266d8d62f50568c5de10 (diff)
Move BinaryHeap to its own Github project.
Diffstat (limited to 'Common.lean')
-rw-r--r--Common.lean2
1 files changed, 0 insertions, 2 deletions
diff --git a/Common.lean b/Common.lean
index d433fa6..89c9051 100644
--- a/Common.lean
+++ b/Common.lean
@@ -5,5 +5,3 @@ import Common.String
import Common.List
import Common.Char
import Common.Euclid
-import Common.BinaryHeap
-import Common.Nat