Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Adding Lean 4 #247

Open
markusschmaus opened this issue Sep 27, 2023 · 2 comments
Open

Adding Lean 4 #247

markusschmaus opened this issue Sep 27, 2023 · 2 comments

Comments

@markusschmaus
Copy link

Lean 4 has a great VS Code integration. Is it possible to include its syntax highlighting in this plugin?

https://marketplace.visualstudio.com/items?itemName=leanprover.lean4
@KevinBatdorf
Copy link
Owner

Yeah I'll look into it this weekend or if I have time sooner. It could take some time to get merged in though as I have to submit it upstream to the rendering library and wait for them to tag a release. I'll update here though.

@KevinBatdorf
Copy link
Owner

Added here: shikijs/shiki#527

As soon as they tag a release I'll add it to the plugin. Will follow up when that happens

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@KevinBatdorf @markusschmaus