feat: BitVec.getElem_[sub|neg|sshiftRight'|abs]

tobiasgrosser commented 6 days ago

This PR adds lemmas for extracting a given bit of a BitVec obtained via sub/neg/sshiftRight'/abs.

leanprover-community-bot commented 6 days ago

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 799b2b662825e646609963921f2c68489b2e664a --onto 4600bb16fcded0356d20ae232e7f8580c56a5955. (2024-11-19 09:45:55)

kim-em commented 6 days ago

Otherwise LGTM, thanks!

The "Check PR body" CI check is failing, because we've added some new requirements for PRs so we can efficiently build the changelog and release notes.

It currently reports two things:

Error: feat/fix PR must have a `changelog-*` label
Error: feat/fix PR must have changelog summary starting with "This PR ..." as first line.

For BitVec PRs, the relevant label is always changelog-library. One of these labels is required for any feat/fix PR. If it's very minor, consider using either the chore: prefix for the PR title, or add the changelog-no label.

Second, every feat: or fix: PR (except those with changelog-no) must now have a paragraph in the PR description beginning This PR. This text is automatically included in our default release notes. e.g. for this PR I would write

"This PR adds lemmas for extracting a given bit of a BitVec obtain via sub/neg/sshiftRight'/abs."

(or something shorter).

tobiasgrosser commented 5 days ago

changelog-library

tobiasgrosser commented 5 days ago

@kim-em, I updated the PR description. I checked if there is a bot to add the new labels myself, but this does not seem to exist. Can you add the new label as you merge the PR?

kim-em commented 4 days ago

Ah, thanks, I'd forgotten about the label issue. I'll see if we can get that fixed, and in the meantime I can do it.

leanprover / lean4

feat: BitVec.getElem_[sub|neg|sshiftRight'|abs] #6126