feat(src/frontends): order notation by priority in pretty-printer #207
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.
If you have a notation for a special case, e.g.
finset.sum finset.univ
, and a notation for a general case, e.g.finset.sum
, you can now give the special-cased notation a higher priority to ensure it is used by the pretty-printer when applicable.When deciding how to pretty-print an expression, Lean looks up the notations associated to the head of the expression. It tries them one-by-one until it finds a notation that matches the expression. The order in which they are tried used to be the definition order. This PR changes this ordering to have higher-priority notations first.
Although
notation_entry.priority()
is also used by the parser, it doesn't seem to be set at all in mathlib. I expect that there will be no conflicts between the usage ofpriority
in the parser and in the pretty-printer.