Closed tobiasgrosser closed 1 week ago
I addressed all comments. This now leads to an inconsistency with:
@[bv_toNat] theorem toNat_eq (x y : BitVec n) : x = y ↔ x.toNat = y.toNat :=
Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq
@[bv_toNat] theorem toNat_ne (x y : BitVec n) : x ≠ y ↔ x.toNat ≠ y.toNat := by
rw [Ne, toNat_eq]
would you like me to write a follow-up PR to address this inconsistency?
I addressed all comments. This now leads to an inconsistency with:
@[bv_toNat] theorem toNat_eq (x y : BitVec n) : x = y ↔ x.toNat = y.toNat := Iff.intro (congrArg BitVec.toNat) eq_of_toNat_eq @[bv_toNat] theorem toNat_ne (x y : BitVec n) : x ≠ y ↔ x.toNat ≠ y.toNat := by rw [Ne, toNat_eq]
would you like me to write a follow-up PR to address this inconsistency?
Oops, thanks for noticing that! Yes, such a PR would be great.
Mathlib CI status (docs):
nightly-with-mathlib
branch. Trygit rebase e0c1afd12d4fc6b0e520774959aed06bf122aba9 --onto e362b50fa95d6823e59dd706803a93c25e888535
. (2024-05-06 08:41:28)nightly-with-mathlib
branch. Trygit rebase e0c1afd12d4fc6b0e520774959aed06bf122aba9 --onto 883a3e752d78cf0d30628817379a6001252b5595
. (2024-05-08 00:12:27)