def lo_val

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqv.bend:39

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/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

39def lo_val(+w: WU.U64, +h: {C.fits(32n, SW.value(w)) == True{} : Bool}) -> {v(X.lo(w)) == SW.value(w) : Nat}:
40  match w:
41    case WU.U64{+l, +hh}:
42      Equal.trans(Nat, v(l), C.low(32n, SW.value(WU.U64{l, hh})), SW.value(WU.U64{l, hh}), Equal.sym(Nat, C.low(32n, SW.value(WU.U64{l, hh})), v(l), WW.low_u(32n, v(l), v(hh), LW.vb(l))), WW.low_fit(32n, SW.value(WU.U64{l, hh}), h))