English
testBit(a, n) reports whether the nth binary digit of a is 1; by definition testBit(0, n) = false and testBit(pos p, n) = p.testBit n.
Русский
testBit(a, n) определяет, установлен ли n-й бит числа a; по определению testBit(0, n) = false и testBit(pos p, n) = p.testBit n.
LaTeX
$$$\\mathrm{testBit}(0,n)=\\mathrm{false},\\quad \\mathrm{testBit}(\\mathrm{pos}(p),n)=p.\\mathrm{testBit} n$$$
Lean4
/-- `a.testBit n` is `true` iff the `n`-th bit (starting from the LSB) in the binary representation
of `a` is active. If the size of `a` is less than `n`, this evaluates to `false`. -/
def testBit : Num → Nat → Bool
| 0, _ => false
| pos p, n => p.testBit n
