From bb55db1e81149b7f3a58c2cd723c096883b66ab4 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 31 Jan 2006 13:29:40 +0000 Subject: [PATCH] /me finished reviewing ... --- helm/papers/matita/matita2.tex | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex index 3c9bd720b..907573f0c 100644 --- a/helm/papers/matita/matita2.tex +++ b/helm/papers/matita/matita2.tex @@ -1851,18 +1851,19 @@ tactical not atomically. \section{Standard library} \label{sec:stdlib} -\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{} -can be read, checked and referenced in further developments. -However, in order to test the actual usability of the system, a -new library of results has been started from scratch. In this case, -of course, we wrote (and offer) the source script files, -while, in the case of \COQ, \MATITA{} may only rely on XML files of -\COQ{} objects. +\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{} can be +read, checked and referenced in further developments. However, in order to test +the actual usability of the system, a new library of results has been started +from scratch. In this case, of course, we wrote (and offer) the source scripts, +while in the case of \COQ{} \MATITA{} may only rely on XML files of \COQ{} +objects. + The current library just comprises about one thousand theorems in elementary aspects of arithmetics up to the multiplicative property for Eulers' totient function $\phi$. + The library is organized in five main directories: \texttt{logic} (connectives, -quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type +quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type constructors), \texttt{nat} (natural numbers), \texttt{Z} (integers), \texttt{Q} (rationals). The most complex development is \texttt{nat}, organized in 25 scripts, listed in Tab.~\ref{tab:scripts}. @@ -1886,7 +1887,7 @@ scripts, listed in Tab.~\ref{tab:scripts}. We do not plan to maintain the library in a centralized way, as most of the systems do. On the contrary we are currently -developing wiki-technologies to support a collaborative +developing wiki-technologies to support collaborative development of the library, encouraging people to expand, modify and elaborate previous contributions. -- 2.39.2