New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore: fix some @[ext] attribute #11494
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks reasonable; thank you for doing this.
I haven't verified that the newly generated ext lemma matches the previous, manually written one. (If you have, this would be useful to know.)
bors merge Thanks! |
This PR contains 2 changes: 1. Order/Interval.lean: Add `@[ext (flat := false)]`, which addressed the porting notes. 2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in leanprover-community/batteries#159). 3. Algebra/Order/Interval.lean updated now that `ext_iff`'s namespace is changed due to 1. Partially addresses #11182
Build failed: |
bors d+ |
✌️ casavaca can now approve this pull request. To approve and merge a pull request, simply reply with |
6ac1478
to
bd0b323
Compare
bors r+ |
This PR contains 2 changes: 1. Order/Interval.lean: Add `@[ext (flat := false)]`, which addressed the porting notes. 2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in leanprover-community/batteries#159). 3. Algebra/Order/Interval.lean updated now that `ext_iff`'s namespace is changed due to 1. Partially addresses #11182
Pull request successfully merged into master. Build succeeded: |
This PR contains 2 changes: 1. Order/Interval.lean: Add `@[ext (flat := false)]`, which addressed the porting notes. 2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in leanprover-community/batteries#159). 3. Algebra/Order/Interval.lean updated now that `ext_iff`'s namespace is changed due to 1. Partially addresses #11182
This PR contains 2 changes: 1. Order/Interval.lean: Add `@[ext (flat := false)]`, which addressed the porting notes. 2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in leanprover-community/batteries#159). 3. Algebra/Order/Interval.lean updated now that `ext_iff`'s namespace is changed due to 1. Partially addresses #11182
This PR contains 2 changes: 1. Order/Interval.lean: Add `@[ext (flat := false)]`, which addressed the porting notes. 2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in leanprover-community/batteries#159). 3. Algebra/Order/Interval.lean updated now that `ext_iff`'s namespace is changed due to 1. Partially addresses #11182
This PR contains 2 changes: 1. Order/Interval.lean: Add `@[ext (flat := false)]`, which addressed the porting notes. 2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in leanprover-community/batteries#159). 3. Algebra/Order/Interval.lean updated now that `ext_iff`'s namespace is changed due to 1. Partially addresses #11182
This PR contains 2 changes: 1. Order/Interval.lean: Add `@[ext (flat := false)]`, which addressed the porting notes. 2. Matrix/Basic.lean: the porting notes were no longer true, as everything still works after reverting to the original code (this was fixed in leanprover-community/batteries#159). 3. Algebra/Order/Interval.lean updated now that `ext_iff`'s namespace is changed due to 1. Partially addresses #11182
This PR contains 2 changes:
@[ext (flat := false)]
, which addressed the porting notes.ext_iff
's namespace is changed due to 1.Partially addresses #11182