Overview Repositories Revisions Requests Users Attributes Meta

Formalization of floating point numbers for Coq

Edit Package flocq

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

  • Developed at science
  • 1 derived packages
  • Download package
  • osc -A https://api.opensuse.org checkout openSUSE:Factory/flocq && cd $_
  • Create Badge
Refresh
Refresh
Source Files
Filename Size Changed
flocq-4.2.0.tar.gz 0000451654 441 KB
flocq-rpmlintrc 0000000255 255 Bytes
flocq.changes 0000003780 3.69 KB
flocq.spec 0000004398 4.29 KB
Latest Revision
Dominique Leuenberger's avatar Dominique Leuenberger (dimstar_suse) accepted request 1189653 from Aaron Puchert's avatar Aaron Puchert (aaronpuchert) (revision 8) 
- Update to version 4.2.0.
  * Added SF2B' as a proof-free variant of SF2B.
  * Fixed installation of Pff2Flocq.
  * Ensured compatibility from Coq 8.12 to 8.20.
Comments 0
openSUSE Build Service is sponsored by
Places