[Merged by Bors] - fix: set big-operator parsing precedence to 67 #1723
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
jcommelin
reviewed
Jan 20, 2023
| @@ -119,14 +119,14 @@ macro_rules (kind := bigprod) | |||
|
|
|||
| /-- `∑ x in s, f x` is notation for `Finset.sum s f`. It is the sum of `f x`, | |||
| where `x` ranges over the finite set `s`. -/ | |||
| syntax (name := bigsumin) "∑ " extBinder "in " term "," term : term | |||
| syntax (name := bigsumin) "∑ " extBinder "in " term "," term:51 : term | |||
There was a problem hiding this comment.
The library note around lines 84~100 above suggests that we use precedence level 67 everywhere. Should that also work in Lean 4?
dwrensha
changed the title
|
Thanks 🎉 bors merge |
github-actions
bot
added
ready-to-merge
bors bot
pushed a commit
that referenced
this pull request
Jan 20, 2023
Sets all big-operator precedences to 67, in keeping with the existing library note and with lean 3. https://github.com/leanprover-community/mathlib4/blob/82cf1905168dc57e7d95ce5576b7991b31e4f6ea/Mathlib/Algebra/BigOperators/Basic.lean#L89-L93 Fixes downstream code that relied on the wrong precedences. In all cases, the change in this PR makes the code match the parenthesization of the mathlib3 version. I came across this problem when I tried to write ```lean lemma sum_range_square (n : ℕ) : ∑i in Finset.range n, (i+1)^2 = n * (n + 1) * (2*n + 1)/6 := sorry ``` and I got the error ``` failed to synthesize instance AddCommMonoid Prop ``` This PR fixes that error, so that my example successfully parses as expected.
|
Pull request successfully merged into master. Build succeeded:
|
bors
bot
changed the title
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.
Sets all big-operator precedences to 67, in keeping with the existing library note and with lean 3.
mathlib4/Mathlib/Algebra/BigOperators/Basic.lean
Lines 89 to 93 in 82cf190
Fixes downstream code that relied on the wrong precedences. In all cases, the change in this PR makes the code match the parenthesization of the mathlib3 version.
I came across this problem when I tried to write
and I got the error
This PR fixes that error, so that my example successfully parses as expected.