summaryrefslogtreecommitdiff
path: root/Common.lean
diff options
context:
space:
mode:
authorAndreas Grois <andi@grois.info>2023-12-13 19:43:48 +0100
committerAndreas Grois <andi@grois.info>2023-12-13 19:48:20 +0100
commit3469d1e0e5e44c29484ff2f843c0863afa502eea (patch)
treedd9b52e5e0ab2add89639fbeb775489ffbd1ffd2 /Common.lean
parente6365d2c473815a14e888b827c25596d5b995f43 (diff)
Rename file to BinaryHeap, as it isn't a BTree
Diffstat (limited to 'Common.lean')
-rw-r--r--Common.lean2
1 files changed, 1 insertions, 1 deletions
diff --git a/Common.lean b/Common.lean
index 32b40ec..1eedec8 100644
--- a/Common.lean
+++ b/Common.lean
@@ -5,4 +5,4 @@ import Common.String
import Common.List
import Common.Char
import Common.Euclid
-import Common.BTreeHeap
+import Common.BinaryHeap