From 611c369de1874950682501d4454cce3e73c4d6cd Mon Sep 17 00:00:00 2001 From: Andreas Grois Date: Fri, 29 Nov 2024 23:08:15 +0100 Subject: 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 --- Day12.lean | 2 +- Day14.lean | 4 ++-- Day3.lean | 4 ++-- Day8.lean | 4 ++-- 4 files changed, 7 insertions(+), 7 deletions(-) diff --git a/Day12.lean b/Day12.lean index 25fd28a..a9aa172 100644 --- a/Day12.lean +++ b/Day12.lean @@ -1,5 +1,5 @@ import «Common» -import Lean.Data.HashMap +import Std.Data.HashMap namespace Day12 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 diff --git a/Day3.lean b/Day3.lean index 8bf0874..fd6fbc8 100644 --- a/Day3.lean +++ b/Day3.lean @@ -1,6 +1,6 @@ import «Common» -import Lean.Data.HashSet -import Lean.Data.HashMap +import Std.Data.HashSet +import Std.Data.HashMap namespace Day3 structure Coordinate : Type 0 where diff --git a/Day8.lean b/Day8.lean index 6bb7e99..62dc1fa 100644 --- a/Day8.lean +++ b/Day8.lean @@ -1,6 +1,6 @@ import «Common» -import Lean.Data.HashMap -import Lean.Data.HashSet +import Std.Data.HashMap +import Std.Data.HashSet namespace Day8 -- cgit v1.2.3