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 --- Day3.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Day3.lean') 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 -- cgit v1.2.3