Skip to content

feat: lemmas about operations on finite unsigned integers#7484

Merged
TwoFX merged 12 commits intomasterfrom
markus/intx-arithmetic-1
Mar 18, 2025
Merged

feat: lemmas about operations on finite unsigned integers#7484
TwoFX merged 12 commits intomasterfrom
markus/intx-arithmetic-1

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented Mar 14, 2025

This PR adds some lemmas about operations defined on UIntX

@TwoFX TwoFX added the changelog-library Library label Mar 14, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 14, 2025 14:29 Inactive
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 14, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 14, 2025
Update lean-toolchain for testing leanprover/lean4#7484
37b58cd
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 14, 2025
Update lean-toolchain for testing leanprover/lean4#7484
89dca04
@ghost
Copy link
Copy Markdown

ghost commented Mar 14, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

  • 💥 Mathlib branch lean-pr-testing-7484 build failed against this PR. (2025-03-14 14:55:34) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6a202f5acbac5818997e560c2d954e6d6c6a83f5 --onto d32a7b250ad20477d55034488d89a050fbf70af5. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-18 10:55:44)

@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 14, 2025
@TwoFX TwoFX mentioned this pull request Mar 17, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Mar 18, 2025
@TwoFX
feat: Nat, Fin and BitVec theorems required for unsigned intege…
6a202f5 
…rs (#7522)

This PR splits off the required theory about `Nat`, `Fin` and `BitVec`
from #7484.
@TwoFX TwoFX marked this pull request as ready for review March 18, 2025 10:29
@TwoFX TwoFX requested a review from kim-em as a code owner March 18, 2025 10:29
@TwoFX TwoFX enabled auto-merge March 18, 2025 10:29
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 18, 2025 10:37 Inactive
@TwoFX TwoFX added this pull request to the merge queue Mar 18, 2025
Merged via the queue into master with commit d66abc0 Mar 18, 2025
16 checks passed
@TwoFX TwoFX deleted the markus/intx-arithmetic-1 branch August 4, 2025 07:18
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@TwoFX