Full description
Flocq (Floats for Coq) is a formalization of floating-point arithmetic for
the Coq proof assistant. It provides a comprehensive library of theorems on
a multi-radix multi-precision arithmetic. It also supports efficient
numerical computations inside Coq.