def hlf

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32half.bend:20

import Base

20# The Nat halving the checker can compute structurally (no Nat.div).
21def hlf(n: Nat) -> Nat:
22  match n:
23    case 0n:
24      0n
25    case 1n+p:
26      match p:
27        case 0n:
28          0n
29        case 1n+q:
30          1n+hlf(q)