Language

Package: coq-coquelicot @ 3.2.0

Synopsis

Coq library for Reals

Description

Coquelicot is an easier way of writing formulas and theorem statements, achieved by relying on total functions in place of dependent types for limits, derivatives, integrals, power series, and so on. To help with the proof process, the library comes with a comprehensive set of theorems that cover not only these notions, but also some extensions such as parametric integrals, two-dimensional differentiability, asymptotic behaviors. It also offers some automations for performing differentiability proofs. Moreover, Coquelicot is a conservative extension of Coq's standard library and provides correspondence theorems between the two libraries.

Home page
http://coquelicot.saclay.inria.fr
Location
gnu/packages/coq.scm (line: 372, 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 'mathcomp' does not match package name 'coq-mathcomp'