oneBits — Mathlib

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)

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