def U32Nat.low

bend-osdev-u32@0.1.0.0 · u32.bend:56

import Base

56# the low k bits of x (x mod 2^k), and the rest (x / 2^k, rounded down):
57# x = low(k, x) + 2^k high(k, x)
58def U32Nat.low(k: Nat, +x: Nat) -> Nat:
59  match k:
60    case 0n:
61      0n
62    case 1n+j:
63      Nat.add(U32Nat.odd(x), Nat.double(U32Nat.low(j, U32Nat.half(x))))