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.1.0.tar.gz 0000447412 437 KB
flocq-rpmlintrc 0000000255 255 Bytes
flocq.changes 0000002223 2.17 KB
flocq.spec 0000004120 4.02 KB
Revision 2 (latest revision is 8)
Dominique Leuenberger's avatar Dominique Leuenberger (dimstar_suse) accepted request 980558 from Aaron Puchert's avatar Aaron Puchert (aaronpuchert) (revision 2) 
- Update to version 4.1.0.
  * Added `Bnearbyint` and `Btrunc` in `IEEE754`.
  * Ensured compatibility from Coq 8.12 to 8.16.
- Fix patching of coqdoc invocation, make it more robust.
- Patch up coqdoc invocation also for older Coq versions since they
  don't understand --coqlib_url.
Comments 0
openSUSE Build Service is sponsored by
Places