fix(syntaxes/lean): fix some corner cases, add more scopes #269
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.
This:
punctuation.definition.binder.*.(begin|end).lean
scopes to opening and closing bracespunctuation.separator.type.lean
scopes to:
in bindersvariables
linesinstance {R : Type}
to not considerR
a universe variableexample
to get the new new binder highlightingaxiom
andconstant
to not consume until the next:=