leanprover/LeanInk

Colorization difference

Opened this issue · 0 comments

Description

In our reference manual, triple back ticked lean snippets are colored differently from LeanInk processed snippets:

image

Sometimes I still need a triple back ticked lean snippet because I'm copying something from lean core and I would get weird errors (which results in weird tooltips) if I tried to compile it using leanInk.

Expected behaviour

Would be nice if they were consistently colored.

Reproducing the issue

See my new Applicatives.lean chapter.

Environment information

  • Operating System:
  • Lean version:
  • LeanInk version:
  • Alectryon version:

Suggested fix

Additional Notes