Add Syntax Highlighting for Lean#1446
Merged
sharkdp merged 3 commits intosharkdp:masterfrom Jan 2, 2021
Julian:lean
Merged
Conversation
Julian
added a commit
to Julian/dotfiles
that referenced
this pull request
Dec 23, 2020
Or in case it doesn't get merged...
Covers syntax for Lean 3, an interactive theorem prover at https://leanprover-community.github.io/ whose users mostly use VSCode.
Contributor
Author
|
@sharkdp thanks for the review -- addressed I believe! |
Owner
|
|
Owner
|
Added in bat v0.18. |
Julian
added a commit
to Julian/dotfiles
that referenced
this pull request
Jun 18, 2022
Or in case it doesn't get merged...
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Hello --
Leanis 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!