Documentation

Batteries.Data.BitVec.Lemmas

@[deprecated BitVec.eq_nil]

Alias of BitVec.eq_nil.


Every bitvector of length 0 is equal to nil, i.e., there is only one empty bitvector

sub/neg #

@[deprecated BitVec.toNat_sub]
theorem BitVec.sub_toNat {n : Nat} (x : BitVec n) (y : BitVec n) :
(x - y).toNat = (2 ^ n - y.toNat + x.toNat) % 2 ^ n

Alias of BitVec.toNat_sub.

@[deprecated BitVec.toNat_neg]
theorem BitVec.neg_toNat {n : Nat} (x : BitVec n) :
(-x).toNat = (2 ^ n - x.toNat) % 2 ^ n

Alias of BitVec.toNat_neg.