def cm

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:211

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/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as LW

211def cm(+q: U32, +b: U32, +n: Nat, +hn: {Nat.mul(v(q), v(b)) == n : Nat}, +c: Bool, +hc: {C.fits(32n, n) == c : Bool}) -> {G.ok(U32, G.cmul(~U32, ~I.u32_op, ~I.u32_is, q, b)) == SG.checked(~U32, ~SG.u32_of, 32n, n) : Result<&2, &2, NM.NumError, U32>}:
212  match c:
213    case True{}:
214      +hmo2 = mo_of(q, b, n, hn, True{}, hc)
215      %Equal.sym(Bool, I.u32_is(NM.MulOver{q, b}), False{}, hmo2) : {G.ok(U32, G.fits(U32, _, I.u32_op(NM.Mul{q, b}))) == SG.checked(~U32, ~SG.u32_of, 32n, n) : Result<&2, &2, NM.NumError, U32>}
216      %Equal.sym(Bool, C.fits(32n, n), True{}, hc) : {Done{I.u32_op(NM.Mul{q, b})} == SG.checked_pick(~U32, ~SG.u32_of, n, _) : Result<&2, &2, NM.NumError, U32>}
217      %Equal.sym(U32, I.u32_op(NM.Mul{q, b}), of(n), as_of(I.u32_op(NM.Mul{q, b}), n, Equal.trans(Nat, v(I.u32_op(NM.Mul{q, b})), Nat.mul(v(q), v(b)), n, LW.ops_mul(q, b, hmo2), hn))) : {Done{_} == Done{of(n)} : Result<&2, &2, NM.NumError, U32>}
218      {==}
219    case False{}:
220      +hmo = mo_of(q, b, n, hn, False{}, hc)
221      %Equal.sym(Bool, I.u32_is(NM.MulOver{q, b}), True{}, hmo) : {G.ok(U32, G.fits(U32, _, I.u32_op(NM.Mul{q, b}))) == SG.checked(~U32, ~SG.u32_of, 32n, n) : Result<&2, &2, NM.NumError, U32>}
222      %Equal.sym(Bool, C.fits(32n, n), False{}, hc) : {Fail{NM.Overflow{}} == SG.checked_pick(~U32, ~SG.u32_of, n, _) : Result<&2, &2, NM.NumError, U32>}
223      {==}