def frac52

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:278

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/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL

278def frac52(+x: F.F64) -> {C.fits(52n, SF.frac(x)) == True{} : Bool}:
279  match x:
280    case F.Bits{+xl, +xh}:
281      FL.hF(xl, xh)