Package coq-coquelicot @ 3.0.3

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: 368, column: 2)
License

Lint warnings

LinterMessageLocation
derivation

Report failure to compile a package to a derivation

failed to create i686-linux derivation: path ‘/gnu/store/imq41gd3q2767il9gq6mqh5cv44x09rf-guile-2.2.6.drv’ is not valid
derivation

Report failure to compile a package to a derivation

failed to create armhf-linux derivation: path ‘/gnu/store/9wn798a6w534mnn4f28lglbjmib9n392-zlib-1.2.11.drv’ is not valid
derivation

Report failure to compile a package to a derivation

failed to create aarch64-linux derivation: path ‘/gnu/store/0afbxr7962z9ci6kw840n088qsmyz8lr-guile-2.2.6.drv’ is not valid
derivation

Report failure to compile a package to a derivation

failed to create mips64el-linux derivation: path ‘/gnu/store/aiwgcl5dppar2s8l408bshywjybsy3nd-zlib-1.2.11.drv’ is not valid
derivation

Report failure to compile a package to a derivation

failed to create x86_64-linux derivation: path ‘/gnu/store/1dz7hwpizsbvz88j1g2s4c16ayjy36dz-coq-8.10.2.drv’ is not valid