flocq

The Flocq library provides vernacular files formalizing multi-radix multi-precision fixed- and floating-point arithmetic for the Coq proof assistant.