finer grained imports

sullyj3 · Aug 4, 2024 · 9efeade · 9efeade
1 parent 41c3f83
commit 9efeade
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 3 deletions.
diff --git a/src/Sand/Basic.lean b/src/Sand/Basic.lean
@@ -1,4 +1,3 @@
-import Lean
 import Socket
 import «Sand».Time
 

diff --git a/src/Sand/Message.lean b/src/Sand/Message.lean
@@ -1,4 +1,4 @@
-import Lean
+import Lean.Data.Json.Basic
 import «Sand».Basic
 
 open Lean (Json ToJson FromJson toJson fromJson?)

diff --git a/src/Sand/Time.lean b/src/Sand/Time.lean
@@ -1,4 +1,4 @@
-import Lean
+import Lean.Data.Json.FromToJson
 
 open Lean (ToJson FromJson toJson)