libcoq-corn

Coq Constructive Repository at Nijmegen

Description

This library provides different theories for Coq:
 - an algebraic hierarchy with an axiomatic formalization
of the most common algebraic structures, like setoids, monoids, groups, rings, fields, ordered fields, rings of polynomials and real and complex numbers;
 - a construction of the real numbers satisfying the above
axiomatic description;
 - a proof of the fundamental theorem of algebra;
 - a collection of elementary results on real analysis
 including continuity, differentiability, integration,
 Taylor's theorems and the fundamental theorem of calculus;
 - tools for exact real computations like real numbers,
 functions, integrals, graph of functions and differential
 equations.

Coq is a proof assistant for higher-order logic.

Upload more screenshots

Please help extend the collection of screenshots. Just make a screenshot and upload it here. You don't need to register or anything.

Upload a screenshot

Hint: upload an image here from your clipboard with Ctrl-V


Homepage

https://github.com/coq-community/corn


Install this software package

If the package is available for the distribution you are currently using on your computer then install the software by clicking on…

Install libcoq-corn