def Int.testBit : Int → Nat → Bool

testBit m n returns whether the (n+1) least significant bit is 1 or 0, using the two's complement convention for negative m.

Equations

• (Int.ofNat m).testBit x✝ = m.testBit x✝
• (Int.negSucc m).testBit x✝ = !m.testBit x✝

def Int.ofBits {n : Nat} (f : Fin n → Bool) : Int

Construct an integer from a sequence of bits using little endian convention.

The sign is determined using the two's complement convention: the result is negative if and only if n > 0 and f (n-1) = true.

Equations

• Int.ofBits f = if 2 * Nat.ofBits f < 2 ^ n then Int.ofNat (Nat.ofBits f) else Int.subNatNat (Nat.ofBits f) (2 ^ n)

@[simp]

theorem Int.ofBits_zero (f : Fin 0 → Bool) : Int.ofBits f = 0

@[simp]

theorem Int.testBit_ofBits_lt {n i : Nat} {f : Fin n → Bool} (h : i < n) : (Int.ofBits f).testBit i = f ⟨i, h⟩

@[simp]

theorem Int.testBit_ofBits_ge {n i : Nat} {f : Fin n → Bool} (h : i ≥ n) : (Int.ofBits f).testBit i = decide (Int.ofBits f < 0)

theorem Int.testBit_ofBits {n i : Nat} (f : Fin n → Bool) : (Int.ofBits f).testBit i = if h : i < n then f ⟨i, h⟩ else decide (Int.ofBits f < 0)