@[deprecated BitVec.eq_nil]

theorem BitVec.zero_is_unique (x : BitVec 0) : x = BitVec.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.