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.0.tar.gz 121 KB over 1 year ago Download File
gappalib-coq-coq84.patch 2.7 KB over 5 years ago Download File
gappalib-coq.changes 836 Bytes over 1 year ago Download File
gappalib-coq.spec 2.43 KB over 1 year ago Download File

Comments for home:lorenz:formal (0)