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

Colorization difference #22

Description

@lovettchris

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't working

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions