def sgn_pick

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:309

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

309def sgn_pick(+s: Bool) -> {F.sgn(s) == SF.pick(U32, s, 2147483648, 0) : U32}:
310  match s:
311    case True{}:
312      Equal.trans(U32, F.sgn(True{}), 2147483648, SF.pick(U32, True{}, 2147483648, 0), {==}, Equal.sym(U32, SF.pick(U32, True{}, 2147483648, 0), 2147483648, pk_t(U32, 2147483648, 0)))
313    case False{}:
314      Equal.trans(U32, F.sgn(False{}), 0, SF.pick(U32, False{}, 2147483648, 0), {==}, Equal.sym(U32, SF.pick(U32, False{}, 2147483648, 0), 0, pk_f(U32, 2147483648, 0)))