# Lemmas about bitwise operations on integers. #

Possibly only of archaeological significance.

`testBit m n`

returns whether the `(n+1)ˢᵗ`

least significant bit is `1`

or `0`

## Equations

- Int.testBit x x = match x, x with | Int.ofNat m, n => Nat.testBit m n | Int.negSucc m, n => !Nat.testBit m n

`Int.natBitwise`

is an auxiliary definition for `Int.bitwise`

.

## Equations

- Int.natBitwise f m n = bif f false false then Int.negSucc (Nat.bitwise' (fun x y => !f x y) m n) else ↑(Nat.bitwise' f m n)

`Int.bitwise`

applies the function `f`

to pairs of bits in the same position in
the binary representations of its inputs.

## Equations

- One or more equations did not get rendered due to their size.

`shiftr m n`

produces a integer whose binary representation
is obtained by right-shifting the binary representation of `m`

by `n`

places

## Equations

- Int.shiftr m n = Int.shiftl m (-n)