diff --git a/src/examples/SubVerso/Examples/Env.lean b/src/examples/SubVerso/Examples/Env.lean index 17f8705..d07336d 100644 --- 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 index f2e8342..8dbc337 100644 --- 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