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.4.6.tar.gz
sha512=bb9c431d320d9c66998ec02ba7d459ee3f00cb7b16f89e57f3d7eb4b89cd3c9254e98e3906a8dfac31f73e5a32918ad12eaeaf7504750d3bfdce878913b745d3

Description

Tags

keyword:floating-point arithmetic keyword:interval arithmetic keyword:decision procedure category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:Gappa date:2021-01-04

Published: 04 Jan 2021

Dependencies (6)

  1. conf-clang build
  2. conf-g++ build
  3. coq-flocq >= "3.0" & < "4~"
  4. coq >= "8.8.1" & < "8.14~"
  5. ocamlfind build
  6. ocaml

Dev Dependencies (1)

  1. conf-autoconf build & dev

Used by

None

Conflicts

None