def ms_eq

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

import Base
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/instances.bend as I

1019def ms_eq(+bit: Bool, +b: U32, +bok: Bool, +a: U32, +aok: Bool) -> {G.mul_st(~U32, ~I.u32_op, ~I.u32_is, bit, b, bok, (a, aok)) == (ms_a(bit, a, b), ms_ok(bit, a, aok, b, bok)) : U32 & Bool}:
1020  match bit:
1021    case True{}:
1022      {==}
1023    case False{}:
1024      {==}