shiftr — Mathlib

English

Right-shift the binary representation of a PosNum.

Русский

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

LaTeX

$$def shiftr : PosNum → Nat → Num | p, 0 => Num.pos p | 1, _ => 0 | bit0 p, n + 1 => shiftr p n | bit1 p, n + 1 => shiftr p n$$

Lean4

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

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