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

@[match_pattern]

def BitVec.ofNat (n i : Nat) : BitVec n

The bitvector with value i mod 2^n.

Conventions for notations in identifiers:

• The recommended spelling of 0#n in identifiers is zero (not ofNat_zero).

• The recommended spelling of 1#n in identifiers is one (not ofNat_one).

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)