forked from math-comp/math-comp
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge only after solving issue math-comp#361
- Loading branch information
1 parent
4142d98
commit 59895af
Showing
1 changed file
with
1 addition
and
105 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,106 +1,2 @@ | ||
| <!doctype html> | ||
| <html> | ||
| <head> | ||
| <meta charset="utf-8"> | ||
| <meta http-equiv="X-UA-Compatible" content="chrome=1"> | ||
| <title>Mathematical Components</title> | ||
|
|
||
| <link rel="stylesheet" href="stylesheets/styles.css"> | ||
| <link rel="stylesheet" href="stylesheets/github-light.css"> | ||
| <meta name="viewport" content="width=device-width"> | ||
| <!--[if lt IE 9]> | ||
| <script src="//html5shiv.googlecode.com/svn/trunk/html5.js"></script> | ||
| <![endif]--> | ||
| </head> | ||
| <body> | ||
| <div class="wrapper"> | ||
| <header> | ||
| <h1>Mathematical Components</h1> | ||
| <p> Libraries of formalized mathematics</p> | ||
|
|
||
| <p class="view"><a href="https://github.com/math-comp/math-comp">View the Project on GitHub <small>math-comp/math-comp</small></a></p> | ||
|
|
||
|
|
||
| <!-- <ul> --> | ||
| <!-- <li><a href="https://github.com/math-comp/math-comp/zipball/master">Download <strong>ZIP File</strong></a></li> --> | ||
| <!-- <li><a href="https://github.com/math-comp/math-comp/tarball/master">Download <strong>TAR Ball</strong></a></li> --> | ||
| <!-- <li><a href="https://github.com/math-comp/math-comp">View On <strong>GitHub</strong></a></li> --> | ||
| <!-- </ul> --> | ||
| </header> | ||
|
|
||
| <section> | ||
| <h3> | ||
| <a id="about" class="anchor" href="#about" aria-hidden="true"><span class="octicon octicon-link"></span></a>About</h3> | ||
|
|
||
| <p> The Mathematical Components library for | ||
| <a href="http://coq.inria.fr">Coq</a> has its origins in | ||
| the formal proof of the Four Colour Theorem. Since then it has grown | ||
| to cover many areas of mathematics and has been used for | ||
| large scale projects like the formal proof of the Odd Order Theorem. | ||
| </p><p> | ||
| The library is written using the Ssreflect proof language that is an integral | ||
| part of the distribution. | ||
| </p> | ||
|
|
||
| <h3> | ||
| <a id="releases" class="anchor" href="#releases" aria-hidden="true"><span class="octicon octicon-link"></span></a>Getting the library</h3> | ||
|
|
||
| <p> The current stable release of the | ||
| Mathematical Components library can be | ||
| <a href="https://github.com/math-comp/math-comp/releases">downloaded from github</a>. | ||
| <br/> | ||
| Older versions of the library are available | ||
| in the <a href="http://ssr.msr-inria.inria.fr/FTP/">historic archive</a>. | ||
| </p> | ||
|
|
||
| <h3> | ||
| <a id="documentation" class="anchor" href="#documentation" aria-hidden="true"><span class="octicon octicon-link"></span></a>Documentation</h3> | ||
|
|
||
| <p> | ||
| Each source files features a documentation header which | ||
| describes the concepts and notations introduced in that file. | ||
| The <a href="htmldoc/index.html">coqdoc presentation</a> of the source files can be browsed online. | ||
| </p> | ||
| <p> | ||
| The <a href="htmldoc/libgraph.html">library graph</a> can be browsed interactively. | ||
| </p> | ||
| <p> | ||
| The Ssreflect language comes with a dedicated | ||
| <a href="http://hal.inria.fr/inria-00258384/en">reference manual</a>. | ||
| </p> | ||
| <p>We also wrote a <a href="https://math-comp.github.io/mcb/">book</a> introducing the techniques for writing | ||
| algorithms and proofs and describing the design ideas of the library. | ||
| </p> | ||
| <h3> | ||
| <a id="contact" class="anchor" href="#contact" aria-hidden="true"><span class="octicon octicon-link"></span></a>Contact</h3> | ||
|
|
||
| <p> | ||
| Interested? | ||
| <a href="mailto:sympa@inria.fr?subject=SUBSCRIBE%20ssreflect">Subscribe to the ssreflect mailing list</a> | ||
| and let us know what you are using our libraries for, ask questions, etc. | ||
| You can also browse the <a href="https://sympa.inria.fr/sympa/arc/ssreflect">archives of the list</a> or consult the | ||
| <a href="https://sympa.inria.fr/sympa/info/ssreflect">general information page</a>. | ||
| </p> | ||
| <h3> | ||
| <a id="authors-and-contributors" class="anchor" href="#authors-and-contributors" aria-hidden="true"><span class="octicon octicon-link"></span></a>Authors and Contributors</h3> | ||
|
|
||
| <p> The Mathematical Components library and the Ssreflect proof language | ||
| are developed by the | ||
| <a href="http://www.msr-inria.fr/projects/mathematical-components-2/">Mathematical Components team</a>, at the | ||
| <a href="http://www.msr-inria.fr/">Inria -- Microsoft Research Joint Centre</a>. | ||
| </p> | ||
| <p style="text-align:center;"> | ||
| <a href="http://www.msr-inria.fr/"><img src="./logo-MS-Research-Inria-Joint-Centre.png" alt="Microsoft Research - Inria Joint Centre" style="width:50%;margin-left:auto;margin-right:auto;"/></a> | ||
| </p> | ||
|
|
||
| </section> | ||
|
|
||
| <footer> | ||
| <p><small>Theme by <a href="https://github.com/orderedlist">orderedlist</a></small></p> | ||
| </footer> | ||
|
|
||
| </div> | ||
| <script src="javascripts/scale.fix.js"></script> | ||
|
|
||
| </body> | ||
| </html> | ||
| <html><head><meta http-equiv="refresh" content="0; url=http://math-comp.github.io/" /></head></html> |