def ap

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addf.bend:44

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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

44def ap(+x: F.F64, +y: F.F64, +same: Bool) -> {F.add_pick(x, y, same) == SF.pick(F.F64, same, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))) : F.F64}:
45  match same:
46    case True{}:
47      Equal.trans(F.F64, F.add_pick(x, y, True{}), F.add_mags(x, y, F.signbit(x)), SF.pick(F.F64, True{}, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))), {==}, Equal.sym(F.F64, SF.pick(F.F64, True{}, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))), F.add_mags(x, y, F.signbit(x)), FR.pk_t(F.F64, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x)))))
48    case False{}:
49      Equal.trans(F.F64, F.add_pick(x, y, False{}), F.sub_mags(x, y, F.signbit(x)), SF.pick(F.F64, False{}, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))), {==}, Equal.sym(F.F64, SF.pick(F.F64, False{}, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))), F.sub_mags(x, y, F.signbit(x)), FR.pk_f(F.F64, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x)))))