# Documentation

## Init.Data.Nat.Bitwise.Basic

theorem Nat.bitwise_rec_lemma {n : Nat} (hNe : n 0) :
n / 2 < n
@[irreducible]
def Nat.bitwise (f : ) (n : Nat) (m : Nat) :
Equations
• One or more equations did not get rendered due to their size.
Instances For
@[extern lean_nat_land]
def Nat.land :
Equations
Instances For
@[extern lean_nat_lor]
def Nat.lor :
Equations
Instances For
@[extern lean_nat_lxor]
def Nat.xor :
Equations
Instances For
@[extern lean_nat_shiftl]
Equations
• x.shiftLeft 0 = x
• x.shiftLeft m.succ = (2 * x).shiftLeft m
Instances For
@[extern lean_nat_shiftr]
Equations
• x.shiftRight 0 = x
• x.shiftRight m.succ = x.shiftRight m / 2
Instances For
instance Nat.instAndOp :
Equations
instance Nat.instOrOp :
Equations
instance Nat.instXor :
Equations
Equations
Equations
theorem Nat.shiftLeft_eq (a : Nat) (b : Nat) :
a <<< b = a * 2 ^ b
@[simp]
theorem Nat.shiftRight_zero {n : Nat} :
n >>> 0 = n
theorem Nat.shiftRight_succ (m : Nat) (n : Nat) :
m >>> (n + 1) = m >>> n / 2
theorem Nat.shiftRight_add (m : Nat) (n : Nat) (k : Nat) :
m >>> (n + k) = m >>> n >>> k
theorem Nat.shiftRight_eq_div_pow (m : Nat) (n : Nat) :
m >>> n = m / 2 ^ n

### testBit #

We define an operation for testing individual bits in the binary representation of a number.

def Nat.testBit (m : Nat) (n : Nat) :

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

Equations
Instances For