[ 源代码: flocq ]
软件包:libcoq-flocq(4.1.4-2 以及其他的)
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.