summaryrefslogtreecommitdiff
path: root/Common.lean
diff options
context:
space:
mode:
authorAndreas Grois <andi@grois.info>2023-12-18 20:42:08 +0100
committerAndreas Grois <andi@grois.info>2023-12-18 20:42:08 +0100
commit214f0bdcbe35a9b6e68ae0b78a502fa2faaca5d6 (patch)
treef3d00021dc6830ec572c8851b9db4271018c2fa2 /Common.lean
parent0f942c82d9b1cb74aad2dd667c2d53f63a38d7a2 (diff)
Partial cleanup of Heap
Diffstat (limited to 'Common.lean')
-rw-r--r--Common.lean1
1 files changed, 1 insertions, 0 deletions
diff --git a/Common.lean b/Common.lean
index 1eedec8..d433fa6 100644
--- a/Common.lean
+++ b/Common.lean
@@ -6,3 +6,4 @@ import Common.List
import Common.Char
import Common.Euclid
import Common.BinaryHeap
+import Common.Nat