LogoopenSUSE Build Service > Projects
Sign Up | Log In

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.

Source Files

Filename Size Changed Actions
_service 75 Bytes Download File
gappalib-coq-1.4.0.tar.gz 122 KB Download File
gappalib-coq.changes 1.59 KB Download File
gappalib-coq.spec 2.43 KB Download File

Comments for home:ptrommler:formal (0)

Login required, please login or signup in order to comment