bits — Mathlib

English

bits(p, n) returns the vector of the first n bits of a in LSB order, via a recursive construction.

Русский

bits(p, n) возвращает вектор первых n битов числа p в порядке от младшего к старшему.

LaTeX

$$$\\mathrm{bits} : \\mathrm{SNum} \\to (n : \\mathbb{N}) \\to \\mathrm{List.Vector}\\;\\mathrm{Bool}\\; n$$$

Lean4

/-- `a.bits n` is the vector of the `n` first bits of `a` (starting from the LSB). -/
def bits : SNum → ∀ n, List.Vector Bool n
  | _, 0 => Vector.nil
  | p, n + 1 => head p ::ᵥ bits (tail p) n

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