English
For SNum, testBit is defined by a head-tail recursion: testBit 0 a equals head a, and testBit (n+1) a equals testBit n (tail a).
Русский
У SNum проверка бита задаётся рекурсивно: testBit 0 a равно head a, а testBit (n+1) a равно testBit n (tail a).
LaTeX
$$$\\mathrm{testBit} : \\mathbb{N} \\to \\mathrm{SNum} \\to \\mathrm{Bool},\\quad \\mathrm{testBit}(0,p)=\\mathrm{head}\,p,\\quad \\mathrm{testBit}(n+1,p)=\\mathrm{testBit}(n,\\mathrm{tail}\,p)$$$
Lean4
/-- `SNum.testBit n a` is `true` iff the `n`-th bit (starting from the LSB) of `a` is active.
If the size of `a` is less than `n`, this evaluates to `false`. -/
def testBit : Nat → SNum → Bool
| 0, p => head p
| n + 1, p => testBit n (tail p)
