The Flocq library provides vernacular files formalizing multi-radix multi-precision fixed- and floating-point arithmetic for the Coq proof assistant.
Homepage: http://flocg.gforge.inria.fr/
Repository: https://gitlab.inria.fr/flocq/flocq
Bug tracker: https://gitlab.inria.fr/flocq/flocq/issues
This package is free software; you can redistribute it and/or modify it under the terms of GNU Lesser General Public License (see the COPYING file). Authors are Sylvie Boldo [email protected] and Guillaume Melquiond [email protected].
See the file INSTALL.md.