English
`m <<< n` produces the integer obtained by left-shifting the binary representation of m by n places.
Русский
`m <<< n` даёт целое, полученное сдвигом влево числа m на n позиций.
LaTeX
$$$m \\text{ left-shifted by } n$$$
Lean4
/-- `m <<< n` produces an integer whose binary representation
is obtained by left-shifting the binary representation of `m` by `n` places -/
instance : ShiftLeft ℤ where
shiftLeft
| (m : ℕ), (n : ℕ) => Nat.shiftLeft' false m n
| (m : ℕ), -[n+1] => m >>> (Nat.succ n)
| -[m+1], (n : ℕ) => -[Nat.shiftLeft' true m n+1]
| -[m+1], -[n+1] => -[m >>> (Nat.succ n)+1]