package coq-interval

  1. Overview
  2. No Docs
A Coq tactic for proving bounds on real-valued expressions automatically

Install

Dune Dependency

coqinterval.gitlabpages.inria.fr Edit opam file Versions (26)

Authors

  1. G
    Guillaume Melquiond <guillaume.melquiond@inria.fr>
  2. Ã
    Érik Martin-Dorel <erik.martin-dorel@irit.fr>
  3. P
    Pierre Roux <pierre.roux@onera.fr>
  4. T
    Thomas Sibut-Pinote <thomas.sibut-pinote@inria.fr>

Maintainers

  1. G
    guillaume.melquiond@inria.fr

Sources

interval-4.11.1.tar.gz
sha512=6b22f3f67a14d371d24f4cead9288f17d0dfeba1708b4c7de19cd884abf658fb197af032b88afb6e6e887d6478df19def6ba07799c2b7e6e5225f979785e5d97

Description

Tags

keyword:interval arithmetic keyword:decision procedure keyword:floating-point arithmetic keyword:reflexive tactic keyword:Taylor models category:Mathematics/Real Calculus and Topology category:Computer Science/Decision Procedures and Certified Algorithms/Decision procedures logpath:Interval date:2024-10-21

Published: 22 Oct 2024

Dependencies (7)

  1. conf-clang build
  2. conf-g++ build
  3. coq-coquelicot >= "3.1"
  4. coq-mathcomp-ssreflect >= "1.12"
  5. coq-flocq >= "3.2"
  6. coq-bignums
  7. coq >= "8.13.1" & != "8.19.0"

Dev Dependencies (1)

  1. conf-autoconf build & dev

Used by (7)

  1. coq-algorand < "1.3"
  2. coq-approx-models
  3. coq-infotheo >= "0.7.2"
  4. coq-libvalidsdp >= "1.0.0"
  5. coq-pi-agm >= "1.2.0" & < "1.2.2" | >= "1.2.5"
  6. coq-validsdp >= "1.0.0"
  7. coq-vcfloat >= "2.2"

Conflicts

None