def mul_st_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/float.bend:126

import Base
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 N

126def mul_st_eq(~T: Data, ~op: N.Op<T> -> T, ~test: N.Test<T> -> Bool, ~mo: NoMulOver(~T, ~test), +d: Bool, +b: T, +a: T) -> {G.mul_st(~T, ~op, ~test, d, b, True{}, (a, True{})) == (SG.pick(T, d, op(N.Mul{a, b}), a), True{}) : T & Bool}:
127  match d:
128    case True{}:
129      %Equal.sym(Bool, test(N.MulOver{a, b}), False{}, mo(a, b)) : {(op(N.Mul{a, b}), Bool.and(Bool.and(True{}, True{}), Bool.not(_))) == (op(N.Mul{a, b}), True{}) : T & Bool}
130      {==}
131    case False{}:
132      {==}