F64mulc.mimpl: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulc.bend as F64mulc
Lines 23-24 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mulc.bend&start_line=23&end_line=24

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F

def mimpl(+s: Bool, +a1: Bool, +b1: Bool, +c1: Bool, +a2: Bool, +b2: Bool, +c2: Bool, +r: F.F64) -> F.F64:
  SF.pick(F.F64, a1, SF.pick(F.F64, Bool.or(Bool.or(Bool.not(b1), Bool.and(a2, Bool.not(b2))), Bool.and(c2, b2)), F.nan(), F.inf(s)), SF.pick(F.F64, a2, SF.pick(F.F64, Bool.or(Bool.not(b2), Bool.and(c1, b1)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.or(Bool.and(c1, b1), Bool.and(c2, b2)), F.zero(s), r)))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pick
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=inf
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=nan
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=zero