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