diff options
Diffstat (limited to 'doc/refman/RefMan-lib.tex')
| -rw-r--r-- | doc/refman/RefMan-lib.tex | 35 |
1 files changed, 19 insertions, 16 deletions
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index f9a5f975..f4cd9a6f 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -16,9 +16,9 @@ The \Coq\ library is structured into three parts: (see section~\ref{Require}); \item[User contributions:] Other specification and proof developments - coming from the \Coq\ users' community. These libraries are no - longer distributed with the system. They are available by anonymous - FTP (see section~\ref{Contributions}). + coming from the \Coq\ users' community. These libraries are + available for download at \texttt{http://coq.inria.fr} (see + section~\ref{Contributions}). \end{description} This chapter briefly reviews these libraries. @@ -27,8 +27,8 @@ This chapter briefly reviews these libraries. \label{Prelude} This section lists the basic notions and results which are directly -available in the standard \Coq\ system -\footnote{Most of these constructions are defined in the +available in the standard \Coq\ system\footnote{Most +of these constructions are defined in the {\tt Prelude} module in directory {\tt theories/Init} at the {\Coq} root directory; this includes the modules {\tt Notations}, @@ -155,6 +155,7 @@ Section Projections. Variables A B : Prop. Theorem proj1 : A /\ B -> A. Theorem proj2 : A /\ B -> B. +End Projections. \end{coq_example*} \begin{coq_eval} Abort All. @@ -165,7 +166,6 @@ Abort All. \ttindex{iff} \ttindex{IF\_then\_else} \begin{coq_example*} -End Projections. Inductive or (A B:Prop) : Prop := | or_introl (_:A) | or_intror (_:B). @@ -800,21 +800,24 @@ subdirectories: \begin{tabular}{lp{12cm}} {\bf Logic} & Classical logic and dependent equality \\ {\bf Arith} & Basic Peano arithmetic \\ - {\bf ZArith} & Basic integer arithmetic \\ - {\bf Bool} & Booleans (basic functions and results) \\ + {\bf NArith} & Basic positive integer arithmetic \\ + {\bf ZArith} & Basic relative integer arithmetic \\ + {\bf Bool} & Booleans (basic functions and results) \\ {\bf Lists} & Monomorphic and polymorphic lists (basic functions and results), Streams (infinite sequences defined with co-inductive types) \\ {\bf Sets} & Sets (classical, constructive, finite, infinite, power set, etc.) \\ - {\bf IntMap} & Representation of finite sets by an efficient - structure of map (trees indexed by binary integers).\\ - {\bf Reals} & Axiomatization of Real Numbers (classical, basic functions, - integer part, fractional part, limit, derivative, Cauchy - series, power series and results,... Requires the - \textbf{ZArith} library).\\ + {\bf FSets} & Specification and implementations of finite sets and finite + maps (by lists and by AVL trees)\\ + {\bf IntMap} & Representation of finite sets by an efficient + structure of map (trees indexed by binary integers).\\ + {\bf Reals} & Axiomatization of real numbers (classical, basic functions, + integer part, fractional part, limit, derivative, Cauchy + series, power series and results,...)\\ {\bf Relations} & Relations (definitions and basic results). \\ - {\bf Sorting} & Sorted list (basic definitions and heapsort correctness). \\ + {\bf Sorting} & Sorted list (basic definitions and heapsort correctness). \\ + {\bf Strings} & 8-bits characters and strings\\ {\bf Wellfounded} & Well-founded relations (basic results). \\ \end{tabular} @@ -1094,7 +1097,7 @@ The users' contributions may also be obtained by anonymous FTP from site \verb:ftp.inria.fr:, in directory \verb:INRIA/coq/: and searchable on-line at \url{http://coq.inria.fr/contribs-eng.html} -% $Id: RefMan-lib.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $ +% $Id: RefMan-lib.tex 9312 2006-10-28 21:08:35Z herbelin $ %%% Local Variables: %%% mode: latex |