blob: e849967c99334cbd49be4c958ba500a918ab8539 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
\section{Lists}\label{Lists}
This library includes the following files:
\begin{itemize}
\item {\tt List.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 Reference Manual about implicit
arguments before using it.
\item {\tt ListSet.v} contains definitions and properties of finite
sets, implemented as lists.
\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}
|
