package coq-gappa

  1. Overview
  2. No Docs
A Coq tactic for discharging goals about floating-point arithmetic and round-off errors using the Gappa prover

Install

Dune Dependency

gappa.gitlabpages.inria.fr Edit opam file Versions (17)

Authors

  1. G
    Guillaume Melquiond <guillaume.melquiond@inria.fr>

Maintainers

  1. G
    guillaume.melquiond@inria.fr

Sources

gappalib-coq-1.3.4.tar.gz
md5=9dc92d9edf82364089a6c7d20078059d

Description

Tags

keyword:floating-point arithmetic keyword:interval arithmetic keyword:decision procedure category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures

Published: 18 Jul 2018

Dependencies (3)

  1. coq-flocq >= "2.5" & < "3.0~"
  2. coq >= "8.4pl4" & < "8.9~" & != "8.4.6~camlp4" & != "8.5.0~camlp4" & != "8.5.2~camlp4"
  3. ocaml

Dev Dependencies

None

Used by

None

Conflicts (1)

  1. coq = "8.8.0"