def u32.go

bend-kit-property@0.4.0.0 · shrink.bend:12

import Base

12# (n - d), then (n - d/2), ..., while d > 0; stop tells whether d is 0.
13def u32.go(f: Nat, stop: Bool, +n: U32, +d: U32) -> List<&1, U32>:
14  match f stop:
15    case 0n _:
16      Nil{}
17    case 1n+p True{}:
18      Nil{}
19    case 1n+p False{}:
20      +h = (d >> 1n : U32)
21      (n - d : U32) <> u32.go(p, U32.is_eq(h, 0), n, h)