In our reference manual, triple back ticked lean snippets are colored differently from LeanInk processed snippets:
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.
Description
In our reference manual, triple back ticked lean snippets are colored differently from LeanInk processed snippets:
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
Suggested fix
Additional Notes