English
For every n, bits(n) is the binary expansion of n represented as a list of booleans, with the least significant bit first.
Русский
Для каждого n bits(n) задаёт двоичное представление n в виде списка булевых значений, начиная с наименее значимого бита.
LaTeX
$$$$\text{bits}(n) = (b_0,b_1,\dots,b_t),\quad n=\sum_{i=0}^t b_i 2^i,\ b_i\in\{0,1\}. $$$$
Lean4
/-- `bits n` returns a list of Bools which correspond to the binary representation of n, where
the head of the list represents the least significant bit -/
def bits : ℕ → List Bool :=
binaryRec [] fun b _ IH => b :: IH
