Documentation

Mathlib.Init.Data.Int.Bitwise

Lemmas about bitwise operations on integers. #

Possibly only of archaeological significance.

def Int.div2 :

div2 n = n/2

Equations
• = match x with | => ↑() | =>
def Int.bodd :

bodd n returns true if n is odd

Equations
• = match x with | => | =>
def Int.bit (b : Bool) :

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

Equations
• = bif b then bit1 else bit0
def Int.testBit :

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

Equations
• = match x, x with | , n => | , n => !
def Int.natBitwise (f : ) (m : ) (n : ) :

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

Equations
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.

Equations
• One or more equations did not get rendered due to their size.
def Int.lnot :

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

Equations
• = match x with | => | => m
def Int.lor :

lor takes two integers and returns their bitwise or

Equations
• One or more equations did not get rendered due to their size.
def Int.land :

land takes two integers and returns their bitwise and

Equations
• One or more equations did not get rendered due to their size.
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ᵢ∧ bᵢ to obtain the iᵗʰ bit of the result.

Equations
• One or more equations did not get rendered due to their size.
def Int.lxor' :

lxor' computes the bitwise xor of two natural numbers

Equations
• One or more equations did not get rendered due to their size.
def Int.shiftl :

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

Equations
• One or more equations did not get rendered due to their size.
def Int.shiftr (m : ) (n : ) :

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

Equations