feat: add pp.fieldNotation.generalized for generalized field notation, add @[pp_nodot] attribute
#3737
Conversation
This file contains 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
…` attribute Refactors app delaborator and merges in the projection delaborator to support pretty printing with generalized field notation. Renames option `pp.structureProjections` to `pp.fieldNotation` and adds sub-option `pp.fieldNotation.generalized` to enable/disable generalized field notation. Sets the default value of `pp.fieldNotation.generalized` to false for now since we need a stage0 update first. Adds `@[pp_nodot]` attribute to permanently disable using field notation for a given declaration.
kmill
changed the title
@[pp_nodot] attributepp.fieldNotation.generalized for generalized field notation, add @[pp_nodot] attribute
github-actions
bot
added
the
toolchain-available
|
Mathlib CI status (docs):
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Refactors app delaborator, merging in the projection delaborator, to support pretty printing with generalized field notation.
Renames option
pp.structureProjectionstopp.fieldNotationand adds sub-optionpp.fieldNotation.generalizedto enable/disable generalized field notation. Adds@[pp_nodot]attribute to permanently disable using field notation for a given declaration.For now, the default value of
pp.fieldNotation.generalizedis false since we need a stage0 update to add@[pp_nodot]to some core definitions (such asList.toArray) before updating the tests.Zulip discussion