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 (show merged sources derived from linked package)

Filename Size Changed Actions
_service 75 Bytes over 5 years ago Download File
gappalib-coq-1.3.3.tar.gz 122 KB 5 months ago Download File
gappalib-coq.changes 1.42 KB 5 months ago Download File
gappalib-coq.spec 2.43 KB 5 months ago Download File

Comments for home:lorenz:formal (0)