Skip to content

chore: upstream Nat.binaryRec#799

Closed
astrainfinita wants to merge 2 commits intoleanprover-community:mainfrom
astrainfinita:binaryRec
Closed

chore: upstream Nat.binaryRec#799
astrainfinita wants to merge 2 commits intoleanprover-community:mainfrom
astrainfinita:binaryRec

Conversation

@astrainfinita
Copy link
Copy Markdown
Contributor

@astrainfinita astrainfinita commented May 16, 2024 •
edited
Loading

Since upstreaming to core (leanprover/lean4#3756) is still controversial, I'd like it to be upstreamed to Batteries first.

@ghost ghost added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label May 16, 2024
@fgdorais fgdorais added the WIP work in progress label May 22, 2024
@astrainfinita astrainfinita changed the base branch from nightly-testing to main June 9, 2024 00:56
@astrainfinita astrainfinita marked this pull request as ready for review June 9, 2024 01:02
@astrainfinita
Copy link
Copy Markdown
Contributor Author

astrainfinita commented Jun 9, 2024

awaiting-review

@github-actions github-actions bot added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed WIP work in progress labels Jun 9, 2024
@ghost ghost removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Jun 9, 2024
@astrainfinita astrainfinita mentioned this pull request Jun 9, 2024
Closed
2 tasks
@astrainfinita astrainfinita mentioned this pull request Aug 6, 2024
Closed
2 tasks
@fgdorais fgdorais added the depends on another PR This is stacked on top of another Batteries PR. label Oct 1, 2024
@ghost ghost added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Oct 14, 2024
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 1, 2024
Update Batteries branch for testing leanprover-community/batteries#799
918a68b
@ghost ghost added the breaks-mathlib label Dec 1, 2024
@ghost
Copy link
Copy Markdown

ghost commented Dec 1, 2024

Mathlib CI status (docs):

@ghost ghost removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Dec 1, 2024
@linesthatinterlace
Copy link
Copy Markdown
Contributor

linesthatinterlace commented Sep 30, 2025

Would you be willing to consider upstreaming Nat.div2, Nat.bodd and related theorems and definitions? They would probably want redefining for performance but I think they are good things to have if you are bringing in Nat.bit.

@fgdorais fgdorais mentioned this pull request Sep 30, 2025
Draft
@ghost ghost added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Oct 22, 2025
@astrainfinita
Copy link
Copy Markdown
Contributor Author

astrainfinita commented Mar 22, 2026

Let's redefine them in mathlib first.

@mathlib-merge-conflicts mathlib-merge-conflicts bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Mar 22, 2026
@astrainfinita astrainfinita mentioned this pull request Mar 23, 2026
Open
@github-actions github-actions bot removed the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Mar 23, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

breaks-mathlib depends on another PR This is stacked on top of another Batteries PR.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@astrainfinita @linesthatinterlace @fgdorais