def signbit_value
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as F64bitsimport 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
235def signbit_value(+x: F.F64) -> SF.Signbit.value(x):
236 match x:
237 case F.Bits{+l, +h}:
238 signbit_g(1n, {==}, l, h, 2147483648, {==})
Uses (3)
Used by (24)
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64exp:rwx
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64modf:zs
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf:afin
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addv:add_g
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp:le_gen
- …