Documentation

Std.Data.BitVec.Lemmas

source
@[deprecated BitVec.eq_nil]
theorem BitVec.zero_is_unique (x : BitVec 0) :
x = BitVec.nil

Replaced 2024-02-07.

sub/neg #

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

Replaced 2024-02-06.

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

Replaced 2024-02-06.