lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard
verified publisher icon leanprover

feat: add `popcount` to `bv_decide`

Open luisacicolini opened this issue 1 month ago • 3 comments

This PR adds the circuit to bitblast BitVec.cpop to bv_decide.

luisacicolini avatar Nov 18 '25 08:11 luisacicolini

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cbf6fe5d1be2186da51492658cf1018f0762cc59 --onto 62f2f9229356039356c0469a46d8ecd77be88e2a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-08 17:19:39)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3fdde57e7bec8615f59310d693a56e6f99357aa1 --onto 6a0b0c8273ab560d093494a2daa4dd3088437ad1. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-15 10:28:59)
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-12-18 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-18 08:58:56)

leanprover-community-bot avatar Dec 08 '25 17:12 leanprover-community-bot

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase cbf6fe5d1be2186da51492658cf1018f0762cc59 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-08 17:19:41)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 3fdde57e7bec8615f59310d693a56e6f99357aa1 --onto 646df6ba16b3f68de539a085456c323e160e206d. You can force reference manual CI using the force-manual-ci label. (2025-12-15 10:29:01)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-18 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-18 08:58:57)

leanprover-bot avatar Dec 08 '25 17:12 leanprover-bot

changelog-library

luisacicolini avatar Dec 08 '25 17:12 luisacicolini