def hi_nz

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divv.bend:46

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

46def hi_nz(+b: WU.U64, +hf: {C.fits(32n, SW.value(b)) == False{} : Bool}) -> {U32.is_zero(X.hi(b)) == False{} : Bool}:
47  match b:
48    case WU.U64{+l, +h}:
49      Equal.trans(Bool, U32.is_zero(h), Nat.is_eq(v(h), 0n), False{}, LW.zero_nat(h), hi_nz_c(l, h, hf, Nat.is_eq(v(h), 0n), {==}))