feat: pp.numericTypes option for printing number literals with type ascriptions
#2933
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
github-actions
bot
added
the
toolchain-available
|
Kha
approved these changes
Nov 21, 2023
|
I am a bit concerned about the name |
|
Sebastian suggested that we go through the RFC process for this, so I'll put this back to draft and we can discuss these issues on Zulip. |
kmill
force-pushed
the
pp_numeral_types
branch
from
b5a85ef to
8eed687
Compare
kmill
changed the title
pp.numeralTypes option for printing number literals with type ascriptionspp.numericTypes option for printing number literals with type ascriptions
|
I'm re-opening this now that it's implementing an RFC. Something I checked by hand is that the delaborators ensure that each subexpression is still hoverable in the infoview. |
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Dec 19, 2023
leanprover-community-mathlib4-bot
added
the
builds-mathlib
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Dec 19, 2023
kmill
force-pushed
the
pp_numeral_types
branch
from
8eed687 to
fb25a2d
Compare
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/batteries
that referenced
this pull request
Jan 31, 2024
leanprover-community-mathlib4-bot
added a commit
to leanprover-community/mathlib4
that referenced
this pull request
Jan 31, 2024
kmill
force-pushed
the
pp_numeral_types
branch
from
fb25a2d to
c5d6d51
Compare
|
This looks good.
|
|
@semorrison I added a RELEASES entry. Regarding the RFC, I'm planning on eventually going through the RFCs I've written and copying the explanations to relevant parts of the docs (in future PRs). |
… ascriptions This was a pretty printer option in the Lean 3 community edition, and it was useful for debugging how arithmetic expressions elaborated or have been otherwise transformed. For example, the real numbers have two exponentiation operations (Real -> Real -> Real and Real -> Nat -> Real) and it is helpful knowing at a glance which of these is `x ^ 2`. Closes leanprover#3021
kim-em
force-pushed
the
pp_numeral_types
branch
from
469be42 to
c54c69f
Compare
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.
Implements the pretty printer option
pp.numericTypesfor including a type ascription for numeric literals. For example,(2 : Nat),(-2 : Int), and(-2 / 3 : Rat). This is useful for debugging how arithmetic expressions have elaborated or have been otherwise transformed. For example, with exponentiation is is helpful knowing whether it isx ^ (2 : Nat)orx ^ (2 : Real). This is like the Lean 3 optionpp.numeralTypesbut it has a wider notion of a numeric literal.Also implements the pretty printer option
pp.natLitfor including thenat_litprefix for raw natural number literals.Closes #3021