def U32Nat.high

import bend-osdev-u32@0.1.0.0/u32.bend as U32

import Base

65def U32Nat.high(k: Nat, x: Nat) -> Nat:
66  match k:
67    case 0n:
68      x
69    case 1n+j:
70      U32Nat.high(j, U32Nat.half(x))

Uses (2)