Version using extraction of Flocq
It is used quite differently from the current master:
- Renamed "F" to "Farith" because I think it is not a good practice to not take such toplevel short name.
- The floating points have an arbitrary size but fixed
- To get the same use than master one can do the computation using operation on
Q.tand do the rounding with
Farith.D.roundq : mw:int -> ew:int -> mode -> Q.t -> Q.t