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

@[extern lean_nat_lor]

def Nat.lor : Nat → Nat → Nat

@[extern lean_nat_lxor]

def Nat.xor : Nat → Nat → Nat

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

instance Nat.instOrOpNat : OrOp Nat

instance Nat.instXorNat : Xor Nat

instance Nat.instShiftLeftNat : ShiftLeft Nat

instance Nat.instShiftRightNat : ShiftRight Nat