F64.low_bits: def of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/src/math/f64.bend as F64
Lines 584-591 of bend-collections@1.0.0.0/src/math/f64.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/src/math/f64.bend&start_line=584&end_line=591

import Base

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

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod