shiftr

Mathlib.Data.Num.Bitwise

URI: https://scilib.ai/kg/mathlib#Num.shiftr

English

Right-shift on Num is defined by the function shiftr with cases: shiftr(0, n) = 0 and shiftr(pos p, n) = p >>> n.

Русский

Правый сдвиг для Num задаётся функцией shiftr: shiftr(0, n) = 0 и shiftr(pos p, n) = p >>> n.

LaTeX

$$$\\mathrm{shiftr}(0,n)=0,\\quad \\mathrm{shiftr}(p,n)=p \\\\!>>> n$$$

Lean4

/-- Right-shift the binary representation of a `Num`. -/
def shiftr : Num → Nat → Num
  | 0, _ => 0
  | pos p, n => p >>> n

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

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

Разделы

Аффилиация

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