Language

Package: coq-interval @ 4.0.0

Synopsis

Coq tactics to simplify inequality proofs

Description

Interval provides vernacular files containing tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.

Home page
http://coq-interval.gforge.inria.fr/
Location
gnu/packages/coq.scm (line: 463, column: 2)
License

Lint warnings

LinterMessageLocation
optional-tests

Make sure tests are only run when requested

the 'check' phase should respect #:tests?