def uq.half

bend-osdev-algo@0.1.0.0 · proof_u32.bend:17

import Base

17# n / 2, rounded down
18def uq.half(n: Nat) -> Nat:
19  match n:
20    case 0n:
21      0n
22    case 1n+p:
23      match p:
24        case 0n:
25          0n
26        case 1n+q:
27          1n+uq.half(q)