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

feat: add BitVec.ofFn and lemmas #1078

Open
wants to merge 17 commits into
base: main
Choose a base branch
from
Open

feat: add BitVec.ofFn and lemmas #1078

wants to merge 17 commits into from
+100 −0

Conversation

fgdorais
Copy link
Collaborator

@fgdorais fgdorais commented Dec 23, 2024 •
edited
Loading

@fgdorais fgdorais added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Dec 23, 2024
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Dec 23, 2024
@leanprover-community-mathlib4-bot
Update Batteries branch for testing leanprover-community/batteries#1078
3017df3
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

kim-em
kim-em reviewed Jan 5, 2025
View reviewed changes
Batteries/Data/BitVec.lean Outdated Show resolved Hide resolved
kim-em
kim-em reviewed Jan 5, 2025
View reviewed changes
Batteries/Data/BitVec.lean Outdated Show resolved Hide resolved
kim-em
kim-em reviewed Jan 5, 2025
View reviewed changes
Batteries/Data/BitVec.lean Outdated Show resolved Hide resolved
@kim-em
Copy link
Collaborator

kim-em commented Jan 8, 2025

This seems to have grown into two separate PRs smushed together?

@fgdorais
Copy link
Collaborator Author

fgdorais commented Jan 9, 2025

Yes, I was working on the split earlier today. I will push the prequel PR soon. I'm also inclined to drop the toInt for now. There's a lot of technical issues that I keep bumping into and I can't seem to find reasonable pathways to link all the necessary endpoints.

@fgdorais fgdorais mentioned this pull request Jan 9, 2025
Merged
@fgdorais fgdorais added depends on another PR This is stacked on top of another Batteries PR. and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Jan 9, 2025
@fgdorais
Copy link
Collaborator Author

fgdorais commented Jan 9, 2025

Split completed, Int part postponed to another PR.

kim-em
kim-em reviewed Jan 10, 2025
View reviewed changes
Batteries/Data/BitVec.lean Outdated Show resolved Hide resolved
@fgdorais fgdorais added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed depends on another PR This is stacked on top of another Batteries PR. labels Jan 15, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@kim-em kim-em kim-em left review comments

Assignees
No one assigned
Labels
awaiting-review This PR is ready for review; the author thinks it is ready to be merged. builds-mathlib
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@fgdorais @leanprover-community-bot @kim-em