1
\section{Lists}\label{Lists}
3
This library includes the following files:
7
\item {\tt List.v} contains definitions of (polymorphic) lists,
8
functions on lists such as head, tail, map, append and prove some
9
properties of these functions. Implicit arguments are used in this
10
library, so you should read the Reference Manual about implicit
11
arguments before using it.
13
\item {\tt ListSet.v} contains definitions and properties of finite
14
sets, implemented as lists.
16
\item {\tt TheoryList.v} contains complementary results on lists. Here
17
a more theoretic point of view is assumed : one extracts functions
18
from propositions, rather than defining functions and then prove them.
20
\item {\tt Streams.v} defines the type of infinite lists (streams). It is a
21
coinductive type. Basic facts are stated and proved. The streams are
24
\item {\tt MonoList.v} THIS OLD LIBRARY IS HERE ONLY FOR COMPATIBILITY
25
WITH OLDER VERSIONS OF COQ. THE USER SHOULD USE {\tt List.v} INSTEAD.