Coq support library for gappa
This support library provides vernacular files so that the certificates Gappa generates can be imported by the Coq proof assistant. It also provides a "gappa" tactic that calls Gappa on the current Coq goal. Gappa (Génération Automatique de Preuves de Propriétés Arithmétiques -- automatic proof generation of arithmetic properties) is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic.
Release | Stable | Testing |
---|---|---|
Fedora Rawhide | 1.5.0-2.fc36 | - |
Fedora 35 | 1.4.6-9.fc35 | - |
Fedora 34 | 1.4.6-4.fc34 | - |
You can contact the maintainers of this package via email at
gappalib-coq dash maintainers at fedoraproject dot org
.