Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Library.tex Sprache: Latech

Original von: Coq^©

\documentclass[11pt]{report}

\usepackage[mathletters]{ucs}
\usepackage[utf8x]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{fullpage}
\usepackage{amsfonts}
\usepackage{url}
\usepackage[color]{../../coqdoc}

\input{../common/version}
\input{../common/title}
\input{../common/macros}

\begin{document}

\coverpage{The standard library}%
{\ }
{This material is distributed under the terms of the GNU Lesser
General Public License Version 2.1.}

\tableofcontents

\newpage
% \section*{The \Coq\ standard library}

This document is a short description of the \Coq\ standard library.
This library comes with the system as a complement of the core library
(the {\bf Init} library ; see the Reference Manual for a description
of this library). It provides a set of modules directly available
through the \verb!Require! command.

The standard library is composed of the following subdirectories:
\begin{description}
  \item[Logic]  Classical logic and dependent equality
  \item[Bool]   Booleans (basic functions and results)
  \item[Arith]  Basic Peano arithmetic
  \item[ZArith] Basic integer arithmetic
  \item[Reals]  Classical Real Numbers and Analysis
  \item[Lists]  Monomorphic and polymorphic lists (basic functions and
                  results), Streams (infinite sequences defined
                  with co-inductive types)
  \item[Sets]   Sets (classical, constructive, finite, infinite, power set,
                  etc.)
  \item[Relations] Relations (definitions and basic results).
  \item[Sorting] Sorted list (basic definitions and heapsort
                 correctness).
  \item[Wellfounded] Well-founded relations (basic results).
  \item[Program] Tactics to deal with dependently-typed programs and
    their proofs.
  \item[Classes] Standard type class instances on relations and
    Coq part of the setoid rewriting tactic.
\end{description}

Each of these subdirectories contains a set of modules, whose
specifications (\gallina{} files) have
been roughly, and automatically, pasted in the following pages. There
is also a version of this document in HTML format on the WWW, which
you can access from the \Coq\ home page at
\texttt{http://coq.inria.fr/library}.

\input{Library.coqdoc}

\end{document}

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.