The Coq mailing list

[Guillaume Allais <sbleune AT gmail.com>]

Dear coq-users,

We are glad to announce the first release of the coqtail project [1].

http://sourceforge.net/projects/coqtail/files/

The coqtail project is gathering M1 students of the ENS Lyon who want
to develop mathematical libraries for Coq. We explored various subjects :

- Analysis (Real and Complex)
- Arithmetic
- Well known lemmas [2]

Here is a non-exhaustive list of what you can find in the coqtail sources :

** Analysis
- Organized libraries on sequences over Reals (with landau relations)
- A framework to use Riemannian Integrals

- Definition of the complex field and basic functions on it
- Analysis basis for complex valued functions
- Full support of power series on reals and complex

** Arithmetic
- Fermat's little theorem

- Primality results

** Well known lemmas
- Uncountability of R
- Euler Summation
- The Stirling equivalent of factorial

We hope that these developments will be useful and we will be happy to
have some feedback.

Cheers,

[1] The coqtail project links :
Website : http://coqtail.sourceforge.net/
Source : http://sourceforge.net/projects/coqtail/files/

Wiki : http://sourceforge.net/apps/mediawiki/coqtail/

[2] See http://www.cs.ru.nl/~freek/100/