English
bitwise f on integers extends the bitwise operation defined on naturals and respects sign appropriately.
Русский
побитовая операция bitwise f на целых числах распространяется на натуральные числа и корректно учитывает знак.
LaTeX
$$$\\mathrm{bitwise}: (\\mathsf{Bool} \\to \\mathsf{Bool} \\to \\mathsf{Bool}) \\to \\mathbb{Z} \\to \\mathbb{Z} \\to \\mathbb{Z}$$$
Lean4
/-- `Int.bitwise` applies the function `f` to pairs of bits in the same position in
the binary representations of its inputs. -/
def bitwise (f : Bool → Bool → Bool) : ℤ → ℤ → ℤ
| (m : ℕ), (n : ℕ) => natBitwise f m n
| (m : ℕ), -[n+1] => natBitwise (fun x y => f x (not y)) m n
| -[m+1], (n : ℕ) => natBitwise (fun x y => f (not x) y) m n
| -[m+1], -[n+1] => natBitwise (fun x y => f (not x) (not y)) m n
