feat: change pp.natLit
to be enabled by default
#6439
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 PR changes the default such that raw
Nat
literals always print withnat_lit
.This makes the experience of hovering over
37 : Nat
in the infoview less confusing, as it no longer expands to a term that reads37 : Nat
.In practice, raw natural literals should never appear in user code, and if they do they are indicative of a buggy tactic or
simp
lemma that dropped the requiredOfNat.ofNat
wrapper that literals are supposed to have. Enabling this pretty printer option by default increases the chance of these mistakes being reported by the users affected by such bugs, and will be invisible to users who are unaffected.