def rt

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

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

310def rt(+x: F.F64, +hfin: {Nat.is_lt(SF.efield(x), 2047n) == True{} : Bool}) -> {SF.round(SF.sign(x), SF.mant(x), SF.xexp(x)) == x : F.F64}:
311  rt_c(x, hfin, 1n, {==}, Nat.is_eq(SF.efield(x), 0n), {==})