def low_bits

bend-collections-laws-math@1.0.0.0 · src/math/f64.bend:584

import Base

584# n mod 2^k and n div 2^k by k halvings (no 2^32 constant: the proof
585# checker would expand it in unary)
586def low_bits(k: Nat, +n: Nat) -> Nat:
587  match k:
588    case 0n:
589      0n
590    case 1n+p:
591      Nat.add(Nat.mod(n, 2n), Nat.double(low_bits(p, Nat.div(n, 2n))))