chore: don't import all of Lean

leanprover · Jul 16, 2024 · d4534a1 · d4534a1
1 parent d555157
commit d4534a1
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 2 deletions.
diff --git a/src/examples/SubVerso/Examples/Env.lean b/src/examples/SubVerso/Examples/Env.lean
@@ -1,4 +1,3 @@
-import Lean
 import SubVerso.Highlighting
 
 open Lean

diff --git a/src/highlighting/SubVerso/Highlighting/Code.lean b/src/highlighting/SubVerso/Highlighting/Code.lean
@@ -1,4 +1,3 @@
-import Lean
 import Lean.Widget.TaggedText
 
 import SubVerso.Compat