[ 源代码： flocq ]
软件包：libcoq-flocq（4.1.3-1 以及其他的）
Floating-point arithmetic for Coq
Flocq provides a formalization of floating-point arithmetic for Coq, in the form of a comprehensive library of theorems on a multi-radix multi-precision arithmetic, with efficient numerical computations.
Coq is a proof assistant for higher-order logic.