English
testBit a n is true iff the nth bit in a's binary representation is active; if the size is less than n, it is false.
Русский
testBit a n истинно тогда, когда n-й бит в двоичном представлении a активен; если размер меньше n, ответ ложь.
LaTeX
$$def testBit : PosNum → Nat → Bool
| 1, 0 => true
| 1, _ => false
| bit0 _, 0 => false
| bit0 p, n + 1 => testBit p n
| bit1 _, 0 => true
| bit1 p, n + 1 => testBit p 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 : PosNum → Nat → Bool
| 1, 0 => true
| 1, _ => false
| bit0 _, 0 => false
| bit0 p, n + 1 => testBit p n
| bit1 _, 0 => true
| bit1 p, n + 1 => testBit p n
