def Bits.value

bend-collections-laws-math@1.0.0.0 · spec/math/f64.bend:477

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW

477# the 64-bit pattern: sign, exponent field, fraction
478def Bits.value(+x: F.F64) -> Type:
479  {SW.value(F.to_bits(x)) == Nat.add(pat(x), C.shift(63n, b2n(sign(x)))) : Nat}