English
oneBits n d returns the list of indices of active bits in the binary representation of n, starting from offset d.
Русский
oneBits n d возвращает список индексов активных битов в двоичном представлении n, начиная с смещения d.
LaTeX
$$def oneBits : PosNum → Nat → List Nat
| 1, d => [d]
| bit0 p, d => oneBits p (d + 1)
| bit1 p, d => d :: oneBits p (d + 1)$$
Lean4
/-- `n.oneBits 0` is the list of indices of active bits in the binary representation of `n`. -/
def oneBits : PosNum → Nat → List Nat
| 1, d => [d]
| bit0 p, d => oneBits p (d + 1)
| bit1 p, d => d :: oneBits p (d + 1)