Documentation

Init.Data.Nat.Bitwise.Basic

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

testBit #

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

def Nat.testBit (m n : Nat) :

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

Equations