# Documentation

Mathlib.Init.Data.Int.Bitwise

# Lemmas about bitwise operations on integers. #

Possibly only of archaeological significance.

def Int.div2 :

div2 n = n/2

Instances For
def Int.bodd :

bodd n returns true if n is odd

Instances For
def Int.bit (b : Bool) :

bit b appends the digit b to the binary representation of its integer input.

Instances For
def Int.testBit :

testBit m n returns whether the (n+1)ˢᵗ least significant bit is 1 or 0

Instances For
def Int.natBitwise (f : ) (m : ) (n : ) :

Int.natBitwise is an auxiliary definition for Int.bitwise.

Instances For
def Int.bitwise (f : ) :

Int.bitwise applies the function f to pairs of bits in the same position in the binary representations of its inputs.

Instances For
def Int.lnot :

lnot flips all the bits in the binary representation of its input

Instances For
def Int.lor :

lor takes two integers and returns their bitwise or

Instances For
def Int.land :

land takes two integers and returns their bitwise and

Instances For
def Int.ldiff' :

ldiff' a b performs bitwise set difference. For each corresponding pair of bits taken as booleans, say aᵢ and bᵢ, it applies the boolean operation aᵢ ∧ bᵢ to obtain the iᵗʰ bit of the result.

Instances For
def Int.lxor' :

lxor' computes the bitwise xor of two natural numbers

Instances For

m <<< n produces an integer whose binary representation is obtained by left-shifting the binary representation of m by n places

m >>> n produces an integer whose binary representation is obtained by right-shifting the binary representation of m by n places