def ms_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:1020

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
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

1020def ms_eq(+bit: Bool, +b: WU.U64, +bok: Bool, +a: WU.U64, +aok: Bool) -> {G.mul_st(~WU.U64, ~I.u64_op, ~I.u64_is, bit, b, bok, (a, aok)) == (ms_a(bit, a, b), ms_ok(bit, a, aok, b, bok)) : WU.U64 & Bool}:
1021  match bit:
1022    case True{}:
1023      {==}
1024    case False{}:
1025      {==}