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

@[irreducible]

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

A helper for implementing bitwise operators on Nat.

Each bit of the resulting Nat is the result of applying f to the corresponding bits of the input Nats, up to the position of the highest set bit in either input.

Equations

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

@[extern lean_nat_land]

def Nat.land : Nat → Nat → Nat

Bitwise and. Usually accessed via the &&& operator.

Each bit of the resulting value is set if the corresponding bit is set in both of the inputs.

Equations

• Nat.land = Nat.bitwise and

@[extern lean_nat_lor]

def Nat.lor : Nat → Nat → Nat

Bitwise or. Usually accessed via the ||| operator.

Each bit of the resulting value is set if the corresponding bit is set in at least one of the inputs.

Equations

• Nat.lor = Nat.bitwise or

@[extern lean_nat_lxor]

def Nat.xor : Nat → Nat → Nat

Bitwise exclusive or. Usually accessed via the ^^^ operator.

Each bit of the resulting value is set if the corresponding bit is set in exactly one of the inputs.

Equations

• Nat.xor = Nat.bitwise bne

@[extern lean_nat_shiftl]

def Nat.shiftLeft : Nat → Nat → Nat

Shifts the binary representation of a value left by the specified number of bits. Usually accessed via the <<< operator.

Examples:

• 1 <<< 2 = 4
• 1 <<< 3 = 8
• 0 <<< 3 = 0
• 0xf1 <<< 4 = 0xf10

Equations

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

@[extern lean_nat_shiftr]

def Nat.shiftRight : Nat → Nat → Nat

Shifts the binary representation of a value right by the specified number of bits. Usually accessed via the >>> operator.

Examples:

• 4 >>> 2 = 1
• 8 >>> 2 = 2
• 8 >>> 3 = 1
• 0 >>> 3 = 0
• 0xf13a >>> 8 = 0xf1

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 b : Nat) : a <<< b = a * 2 ^ b

@[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) : m >>> (n + k) = m >>> n >>> k

theorem Nat.shiftRight_eq_div_pow (m n : Nat) : m >>> n = m / 2 ^ n

theorem Nat.shiftRight_eq_zero (m n : Nat) (hn : m < 2 ^ n) : m >>> n = 0

theorem Nat.shiftRight_le (m n : Nat) : m >>> n ≤ m

testBit

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

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

Returns true if the (n+1)th least significant bit is 1, or false if it is 0.

Equations

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