package coq-flocq
A formalization of floating-point arithmetic for the Coq system
Install
Dune Dependency
Authors
Maintainers
Sources
flocq-4.2.2.tar.gz
sha512=8afd91b74133dcce17a78aa923ad7fcedefeb46bf1f71b78e4e4c1900b936ebe5129924c7353c2728b4879601b44686ece98af89e2e779199bd3ccb77139c6f9
Description
Dependencies (7)
-
conf-clang
build -
conf-g++
build -
ocaml
build - rocq-stdlib
- coq-stdlib
-
coq-core
>= "8.17" -
coq
>= "8.15" & < "8.17"
Dev Dependencies (1)
-
conf-autoconf
build & dev
Used by (18)
-
coq-compcert
>= "3.7~coq-platform" & < "3.7" | >= "3.11" -
coq-compcert-32
>= "3.11" -
coq-compcert-64
< "3.7" -
coq-flocq-quickchick
>= "1.0.1" -
coq-gappa
>= "1.4.0" & < "1.4.4" | >= "1.5.0" -
coq-interval
>= "3.4.0" & < "4.0.0" | >= "4.3.0" -
coq-libvalidsdp
>= "0.6.0" - coq-num-analysis
-
coq-qcert
= "1.0.9" -
coq-validsdp
< "1.1.0" - coq-vcfloat
- coq-vellvm
-
coq-vst
>= "2.6" - coq-vst-32
- coq-vst-64
- coq-vst-lib
- rocq-num-analysis-lebesgue
- rocq-vellvm
Conflicts
None
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>
On This Page