def hp32

bend-collections-laws-crypto@1.0.0.0 · proofs/math/u64/u64div.bend:56

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD

56def hp32(+k: Nat, x: U32) -> Nat:
57  match x:
58    case U32{w}:
59      WD.hi_part(32n, k, w)