Language

Package: coq-interval @ 4.3.1

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
https://coqinterval.gitlabpages.inria.fr/
Location
gnu/packages/coq.scm (line: 453, column: 2)
License

Lint warnings

LinterMessageLocation
optional-tests

Make sure tests are only run when requested

the 'check' phase should respect #:tests?
input-labels

Identify input labels that do not match package names

label 'flocq' does not match package name 'coq-flocq'
input-labels

Identify input labels that do not match package names

label 'bignums' does not match package name 'coq-bignums'
input-labels

Identify input labels that do not match package names

label 'coquelicot' does not match package name 'coq-coquelicot'
input-labels

Identify input labels that do not match package names

label 'mathcomp' does not match package name 'coq-mathcomp'