Add a lexer for Lean 4 by eric-wieser · Pull Request #2618 · pygments/pygments
mentioned this pull request
Kha and others added 4 commits
December 30, 2023 22:53
There is no need for `re.UNICODE` any more, or `u` prefixes.
The version and url information no longer lives in the docstring.
This allows a lean4 version of the lean3 test to be committed
* Use `Whitespace` not `Text` for Whitespace * Use a single token for an entire multiline comment, not one per character * Fix brace-matching for `@[attr]` syntax * Add docstring highlighting
This also corrects the integer parser to not include field projections
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