Coq library for Reals
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.
| Linter | Message | Location |
|---|---|---|
| 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' |