Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: show that BitVec is a commutative ring #8711

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - feat: show that BitVec is a commutative ring #8711

wants to merge 28 commits into from

Conversation

alexkeizer
Copy link
Collaborator

@alexkeizer alexkeizer commented Nov 29, 2023 •
edited
Loading

@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Nov 29, 2023
@alexkeizer alexkeizer added the WIP Work in progress label Nov 29, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) labels Nov 30, 2023
@eric-wieser
Copy link
Member

maintainer merge

I pushed some cleanups, so someone should give this a final look over

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by eric-wieser.

@alexkeizer
Copy link
Collaborator Author

This PR will probably need to wait, I just noticed the std bump in #8700 changes a lot of the BitVector definitions and breaks some of the trivial proofs rfl here. Since #8700 seems to be higher priority, I propose we wait until that has been merged, then fix this PR.

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Nov 30, 2023
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Dec 1, 2023
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@tobiasgrosser tobiasgrosser added the awaiting-author A reviewer has asked the author a question or requested changes label Dec 10, 2023
@alexkeizer
WIP: fix ofFin_intCast
ee86242 
Std changed the definition of `BitVec.ofInt`, breaking `ofFin_intCast`. This commit is a first step towards fixing this proof
@tobiasgrosser @github-actions
Update Mathlib/Data/BitVec/Lemmas.lean
8367843 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
eric-wieser
eric-wieser approved these changes Dec 15, 2023
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

Thanks!

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Dec 15, 2023

✌️ alexkeizer can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@alexkeizer
Copy link
Collaborator Author

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Dec 15, 2023
@alexkeizer @tobiasgrosser @eric-wieser
feat: show that BitVec is a commutative ring (#8711)
1250aa8 
Co-authored-by: Tobias Grosser <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
@alexkeizer
Copy link
Collaborator Author

Thanks for the quick final review @eric-wieser!

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Dec 15, 2023

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: show that BitVec is a commutative ring [Merged by Bors] - feat: show that BitVec is a commutative ring Dec 15, 2023
@mathlib-bors mathlib-bors bot closed this Dec 15, 2023
@mathlib-bors mathlib-bors bot deleted the bitvec-ring branch December 15, 2023 16:56
awueth pushed a commit that referenced this pull request Dec 19, 2023
@eric-wieser @awueth
chore: bump std (#8897)
1ec5ce1 
Since this bump does not include leanprover-community/batteries#427 (in order to avoid having to handle the intermediate commits all at once), we temporarily remove the single use of a `∀ i ∉ s,` binder, and the two tests of it.

We can revert these changes in a later Std bump, once we've address the other awkward bumps inbetween.

This unblocks #8711.
awueth pushed a commit that referenced this pull request Dec 19, 2023
@alexkeizer @tobiasgrosser
@eric-wieser @awueth
feat: show that BitVec is a commutative ring (#8711)
3037a13 
Co-authored-by: Tobias Grosser <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@github-actions github-actions[bot] github-actions[bot] left review comments

@tobiasgrosser tobiasgrosser tobiasgrosser left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees

@eric-wieser eric-wieser

Labels
awaiting-author A reviewer has asked the author a question or requested changes delegated
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@alexkeizer @eric-wieser @leanprover-community-mathlib4-bot @tobiasgrosser