source
theorem Nat.bitwise_rec_lemma {n : Nat} (hNe : n ≠ 0) :
n / 2 < n
source
@[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 `Nat`s, 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.

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
instance Nat.instAndOp :
AndOp Nat
Equations

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

source
instance Nat.instOrOp :
OrOp Nat
Equations

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

source
instance Nat.instXorOp :
XorOp Nat
Equations

- Nat.instXorOp = { xor := Nat.xor }

source
instance Nat.instShiftLeft :
ShiftLeft Nat
Equations

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

source
instance Nat.instShiftRight :
ShiftRight Nat
Equations

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

source
theorem Nat.shiftLeft_eq (a b : Nat) :
a <<< b = a * 2 ^ b
source
@[simp]
theorem Nat.shiftRight_zero {n : Nat} :
n >>> 0 = n
source
theorem Nat.shiftRight_succ (m n : Nat) :
m >>> (n + 1) = m >>> n / 2
source
theorem Nat.shiftRight_add (m n k : Nat) :
m >>> (n + k) = m >>> n >>> k
source
theorem Nat.shiftRight_eq_div_pow (m n : Nat) :
m >>> n = m / 2 ^ n
source
theorem Nat.shiftRight_eq_zero (m n : Nat) (hn : m < 2 ^ n) :
m >>> n = 0
source
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.

source
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)

Instances For