package coq-vcfloat

  1. Overview
  2. Homepage
VCFloat: Floating Point Round-off Error Analysis

Install

Dune Dependency

Authors

Maintainers

Sources

v2.3.tar.gz
sha256=daa5a26b65c086eb9014704f53f319594b9348c77d1add2b94437771ecd69ae0

Description

VCFloat is a tool for Coq proofs about floating-point round-off error.

Dependencies (5)

  1. coq-bignums
  2. coq-compcert >= "3.15"
  3. coq-interval >= "4.10.0"
  4. coq-flocq >= "4.1.4" & < "5.0"
  5. coq >= "8.19" & < "8.21~"

Dev Dependencies

None

Used by (1)

  1. coq-vst-lib != "2.13"

Conflicts

None

Rocq

Interactive Theorem Prover