diff --git a/src/verso-manual/VersoManual/InlineLean/Baffler.lean b/src/verso-manual/VersoManual/InlineLean/Baffler.lean new file mode 100644 index 000000000..d71a00b7d --- /dev/null +++ b/src/verso-manual/VersoManual/InlineLean/Baffler.lean @@ -0,0 +1,2 @@ +module +import MultiVerso.NameMap diff --git a/src/verso-manual/VersoManual/InlineLean/Outputs.lean b/src/verso-manual/VersoManual/InlineLean/Outputs.lean index 92aa157d0..1abae6927 100644 --- a/src/verso-manual/VersoManual/InlineLean/Outputs.lean +++ b/src/verso-manual/VersoManual/InlineLean/Outputs.lean @@ -7,6 +7,7 @@ import Lean.Environment import Lean.Message import Lean.Exception import Verso +import VersoManual.InlineLean.Baffler open Lean open SubVerso.Highlighting