theorem Nat.bitwise_rec_lemma {n : Nat} (hNe : n ≠ 0) : n / 2 < n

@[irreducible]

def Nat.bitwise (f : Bool → Bool → Bool) (n : Nat) (m : Nat) : Nat

Equations

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

@[extern lean_nat_land]

def Nat.land : Nat → Nat → Nat

Equations

• Nat.land = Nat.bitwise and

@[extern lean_nat_lor]

def Nat.lor : Nat → Nat → Nat

Equations

• Nat.lor = Nat.bitwise or

@[extern lean_nat_lxor]

def Nat.xor : Nat → Nat → Nat

Equations

• Nat.xor = Nat.bitwise bne

@[extern lean_nat_shiftl]

def Nat.shiftLeft : Nat → Nat → Nat

Equations

• x.shiftLeft 0 = x
• x.shiftLeft m.succ = (2 * x).shiftLeft m

@[extern lean_nat_shiftr]

def Nat.shiftRight : Nat → Nat → Nat

Equations

• x.shiftRight 0 = x
• x.shiftRight m.succ = x.shiftRight m / 2

instance Nat.instAndOp : AndOp Nat

Equations

• Nat.instAndOp = { and := Nat.land }

instance Nat.instOrOp : OrOp Nat

Equations

• Nat.instOrOp = { or := Nat.lor }

instance Nat.instXor : Xor Nat

Equations

• Nat.instXor = { xor := Nat.xor }

instance Nat.instShiftLeft : ShiftLeft Nat

Equations

• Nat.instShiftLeft = { shiftLeft := Nat.shiftLeft }

instance Nat.instShiftRight : ShiftRight Nat

Equations

• Nat.instShiftRight = { shiftRight := Nat.shiftRight }

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) : Bool

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

Equations

• m.testBit n = (1 &&& m >>> n != 0)