Skip to content
This repository has been archived by the owner on Aug 24, 2024. It is now read-only.

Colorization difference #22

Open
lovettchris opened this issue Aug 25, 2022 · 0 comments
Open

Colorization difference #22

lovettchris opened this issue Aug 25, 2022 · 0 comments
Labels
bug Something isn't working

Comments

@lovettchris
Copy link
Contributor

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

@lovettchris lovettchris added the bug Something isn't working label Aug 25, 2022
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant