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 comparison lemmas to bv_normalize #6788

Merged
merged 2 commits into from
Jan 27, 2025
Merged

feat: add comparison lemmas to bv_normalize #6788

merged 2 commits into from
Jan 27, 2025

Conversation

vlad902
Copy link
Contributor

@vlad902 vlad902 commented Jan 27, 2025

This PR teaches bv_normalize that !(x < x) and !(x < 0).

@vlad902
feat: add comparison lemmas to bv_normalize
2f5d344 
This PR teaches bv_normalize that !(x < x) and !(x < 0).
@vlad902 vlad902 requested a review from hargoniX as a code owner January 27, 2025 09:42
@vlad902
Copy link
Contributor Author

vlad902 commented Jan 27, 2025

changelog-language

@github-actions github-actions bot added changelog-language Language features, tactics, and metaprograms toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Jan 27, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 27, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d86a4089444261be04e167b19fe9f4ea0461bf09 --onto 62788395345c7f145714157c138acd0e137ab716. (2025-01-27 10:06:34)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d86a4089444261be04e167b19fe9f4ea0461bf09 --onto 69a73a18fbfa1fc045bfbf1c4cf93b155d4c9387. (2025-01-27 10:44:30)

@hargoniX hargoniX added this pull request to the merge queue Jan 27, 2025
Merged via the queue into leanprover:master with commit 3aea0fd Jan 27, 2025
14 checks passed
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Jan 28, 2025
@vlad902 @luisacicolini
feat: add comparison lemmas to bv_normalize (leanprover#6788)
03dfb7e 
This PR teaches bv_normalize that !(x < x) and !(x < 0).
@nomeata nomeata mentioned this pull request Jan 28, 2025
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX is a code owner

Assignees
No one assigned
Labels
changelog-language Language features, tactics, and metaprograms 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.
3 participants
@vlad902 @leanprover-community-bot @hargoniX