def cmp_pack

bend-collections-laws-math@1.0.0.0 · proofs/math/u64/u64.bend:55

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as U
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W

55def cmp_pack(+alo: U32, +ahi: U32, +blo: U32, +bhi: U32) -> {Word.cmp(64n, W.pack(alo, ahi), W.pack(blo, bhi)) == U.order(U32.cmp(ahi, bhi), U32.cmp(alo, blo)) : Cmp}:
56  match alo ahi blo bhi:
57    case U32{a} U32{b} U32{c} U32{d}:
58      cmp_join(32n, 32n, a, b, c, d)