@[deprecated BitVec.eq_nil]

theorem BitVec.zero_is_unique (x : BitVec 0) : x = BitVec.nil

Replaced 2024-02-07.

sub/neg

@[deprecated BitVec.toNat_sub]

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

Replaced 2024-02-06.

@[deprecated BitVec.toNat_neg]

theorem BitVec.neg_toNat {n : Nat} (x : BitVec n) : (-x).toNat = (2 ^ n - x.toNat) % 2 ^ n

Replaced 2024-02-06.