-
-
Notifications
You must be signed in to change notification settings - Fork 1.2k
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.
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
Add Syntax Highlighting for Lean #1446
Conversation
Or in case it doesn't get merged...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you very much for your contribution!
Could you please add a syntax test (see #1213 for instructions)?
Covers syntax for Lean 3, an interactive theorem prover at https://leanprover-community.github.io/ whose users mostly use VSCode.
@sharkdp thanks for the review -- addressed I believe! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thank you
|
Added in bat v0.18. |
Or in case it doesn't get merged...
Hello --
Lean
is an interactive theorem prover with a decent sized user base (e.g. its Zulip has... around 3,000 folks idling in it). No users really use Sublime Text, the vast majority of its users use VSCode, with a small subset using emacs (and an even smaller subset using other), so as I read it it likely doesn't meet the inclusion criteria, but just checking to be sure the above doesn't affect anything (it not really having any Sublime users). I'm sure you get a bunch of these, so certainly no hard feelings if you close it.Thanks for
bat
!