Package coq-coquelicot @ 3.0.2

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/index.html
Location
gnu/packages/coq.scm (line: 353, column: 2)
License

Lint warnings

LinterMessageLocation
No lint warnings