shiftl

Mathlib.Data.Num.Bitwise

URI: https://scilib.ai/kg/mathlib#PosNum.shiftl

English

Left-shift the binary representation of a PosNum by n bits.

Русский

Левый сдвиг двоичного представления PosNum на n бит.

LaTeX

$$def shiftl : PosNum → Nat → PosNum | p, 0 => p | p, n + 1 => shiftl p.bit0 n$$

Lean4

/-- Left-shift the binary representation of a `PosNum`. -/
def shiftl : PosNum → Nat → PosNum
  | p, 0 => p
  | p, n + 1 => shiftl p.bit0 n

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru