This module exists to provide the very basic BitVec definitions required for Init.Data.UInt.BasicAux.

instance BitVec.instOfNat {n i : Nat} : OfNat (BitVec n) i

theorem BitVec.isLt {w : Nat} (x : BitVec w) : x.toNat < 2 ^ w

Return the bound in terms of toNat.

def BitVec.add {n : Nat} (x y : BitVec n) : BitVec n

Adds two bitvectors. This can be interpreted as either signed or unsigned addition modulo 2^n. Usually accessed via the + operator.

SMT-LIB name: bvadd.

instance BitVec.instAdd {n : Nat} : Add (BitVec n)

def BitVec.sub {n : Nat} (x y : BitVec n) : BitVec n

Subtracts one bitvector from another. This can be interpreted as either signed or unsigned subtraction modulo 2^n. Usually accessed via the - operator.

instance BitVec.instSub {n : Nat} : Sub (BitVec n)