def pick_same
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addv.bend:25
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addv.bend as F64addv
import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
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
25def pick_same(+b: Bool, +r: F.F64) -> {SF.pick(F.F64, b, r, r) == r : F.F64}:
26 match b:
27 case True{}:
28 Equal.trans(F.F64, SF.pick(F.F64, True{}, r, r), r, r, FR.pk_t(F.F64, r, r), {==})
29 case False{}:
30 Equal.trans(F.F64, SF.pick(F.F64, False{}, r, r), r, r, FR.pk_f(F.F64, r, r), {==})