Rounding operator from binary64 into Z?
I'm writing an interpreter in Coq, and I'd like to have a cast/round operator from double-precision floating-point numbers to Coq's BinInt. Is there a function defined in flocq currently doing that? Or the modf function? Or one casting floating-points into rationals?
I know there is such a function in Compcert, but I was unable to find a similar one in Flocq.
Edited by Raphaël Monat