def OfU64.value

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-crypto@1.0.0.0/spec/math/w64.bend as SW

399# the double nearest to an unsigned integer (exact below 2^53)
400def OfU64.value(+w: WU.U64) -> Type:
401  {F.of_u64(w) == round(False{}, SW.value(w), zb()) : F.F64}