blob: 344bba59abc5fc9b143935ff5533a6f86bb867d2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
\section{Lists}\label{Lists}
This library includes the following files:
\begin{itemize}
\item {\tt List.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY
WITH OLDER VERSIONS OF COQS. THE USER SHOULD USE POLYLIST INSTEAD.
\item {\tt PolyList.v} contains definitions of (polymorphic) lists,
functions on lists such as head, tail, map, append and prove some
properties of these functions. Implicit arguments are used in this
library, so you should read the Referance Manual about implicit
arguments before using it.
\item {\tt TheoryList.v} contains complementary results on lists. Here
a more theoric point of view is assumed : one extracts functions
from propositions, rather than defining functions and then prove them.
\item {\tt Streams.v} defines the type of infinite lists (streams). It is a
coinductive type. Basic facts are stated and proved. The streams are
also polymorphic.
\end{itemize}
|
