summaryrefslogtreecommitdiff
path: root/Day14.lean
diff options
context:
space:
mode:
authorAndreas Grois <andi@grois.info>2024-11-29 23:08:15 +0100
committerAndreas Grois <andi@grois.info>2024-11-29 23:08:15 +0100
commit611c369de1874950682501d4454cce3e73c4d6cd (patch)
tree0867e9fe7c67437bd86e9a9fa89f77e341192819 /Day14.lean
parent368c506bc365162cd22f4001ab729ee3df110b79 (diff)
Change all imports from Lean to Std to reduce binary size.
Reduces binary size by more than a factor of 10... https://github.com/leanprover/lean4/issues/5274
Diffstat (limited to 'Day14.lean')
-rw-r--r--Day14.lean4
1 files changed, 2 insertions, 2 deletions
diff --git a/Day14.lean b/Day14.lean
index ad87e68..a7d2279 100644
--- a/Day14.lean
+++ b/Day14.lean
@@ -1,6 +1,6 @@
import «Common»
-import Lean.Data.HashMap
-import Lean.Data.HashSet
+import Std.Data.HashMap
+import Std.Data.HashSet
namespace Day14