def s32_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64conv.bend:234

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/src/math/num.bend as NE
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL

234def s32_c(+a: Bool, +b: Bool, +c: Bool, +n: Nat, +f: Bool, +hf: {C.fits(64n, n) == f : Bool}) -> {f32r(TNR(a, b, c, n, f)) == TNR(a, b, c, n, C.fits(32n, n)) : Result<&2, &2, NE.NumError, Nat>}:
235  match a b c f:
236    case True{} _ _ _:
237      {==}
238    case False{} True{} _ _:
239      {==}
240    case False{} False{} True{} _:
241      {==}
242    case False{} False{} False{} True{}:
243      pn(C.fits(32n, n), n)
244    case False{} False{} False{} False{}:
245      +g = FL.nfit_mono(32n, 64n, n, {==}, hf)
246      Equal.cong(Bool, Result<&2, &2, NE.NumError, Nat>, t => TNR(False{}, False{}, False{}, n, t), False{}, C.fits(32n, n), Equal.sym(Bool, C.fits(32n, n), False{}, g))