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

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

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

@[extern lean_nat_shiftr]

def Nat.shiftRight : Nat → Nat → Nat

Equations

• Nat.shiftRight x 0 = x
• Nat.shiftRight x (Nat.succ m) = Nat.shiftRight x m / 2

instance Nat.instAndOpNat : AndOp Nat

Equations

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

instance Nat.instOrOpNat : OrOp Nat

Equations

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

instance Nat.instXorNat : Xor Nat

Equations

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

instance Nat.instShiftLeftNat : ShiftLeft Nat

Equations

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

instance Nat.instShiftRightNat : ShiftRight Nat

Equations

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

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

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