package coq-interval
A Coq tactic for proving bounds on real-valued expressions automatically
Install
Dune Dependency
Authors
Maintainers
Sources
interval-4.11.4.tar.gz
sha512=5b2ccff32c3d6caa9002455dc472d6c4c8f70337581d038ca432dd92ed90b262b203960a2a62896c12992be2ff2436bf7e6a8ffd3aec625859f47088d262ef00
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:2026-02-23Published: 23 Feb 2026
Dependencies (10)
-
conf-clang
build -
conf-g++
build -
coq-coquelicot
>= "3.1" -
coq-mathcomp-ssreflect
>= "1.12" -
coq-flocq
>= "3.2" - coq-bignums
- coq-stdlib
-
coq-core
!= "8.19.0" -
coq
>= "8.12" & < "8.17~" - ocaml
Dev Dependencies (1)
-
conf-autoconf
build & dev
Used by (8)
-
coq-algorand
< "1.3" - coq-approx-models
-
coq-infotheo
>= "0.7.2" -
coq-libvalidsdp
>= "1.0.0" -
coq-pi-agm
>= "1.2.0" & < "1.2.2" | >= "1.2.5" -
coq-validsdp
>= "1.0.0" & < "1.1.0" -
coq-vcfloat
>= "2.2" - rocq-pi-agm
Conflicts
None
On This Page