lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

Published 20 hours ago • verified publisher icon leanprover

feat: characterize BitVec.toInt in terms of BitVec.toNat

Open bollu opened this issue 1 year ago • 4 comments

This characterizes toInt in terms of toNat.

This PR is stacked on https://github.com/leanprover/lean4/pull/3480 to write the theorems in a style that includes the width zero case.

bollu avatar Feb 24 '24 19:02 bollu

Done, I've made the requested changes. The PR is still in draft mode as it is stacked on top of https://github.com/leanprover/lean4/pull/3480.

bollu avatar Feb 25 '24 21:02 bollu

awaiting-review

bollu avatar Feb 25 '24 22:02 bollu

Mathlib CI status (docs):

  • ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 72d233d181baa183a5288a3a52defd219015e952 --onto 5b15e1a9f3c0d1283df7f2e2f3f1b1dc59f92cf6. (2024-02-25 22:10:54)

leanprover-community-mathlib4-bot avatar Feb 25 '24 22:02 leanprover-community-mathlib4-bot

Looks good. Please ping me once #3480 is in, and conflicts have been resolved here, and I will put this on the queue.

kim-em avatar Feb 29 '24 22:02 kim-em

Superceded by https://github.com/leanprover/lean4/commit/23a202b6bec6348301c65a3260d52f561d3b55fb

bollu avatar Jun 06 '24 14:06 bollu