blob: 22ee38aab53a35041fe039c49b77df9fbc58377e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
\section{Bool}\label{Bool}
The BOOL library includes the following files:
\begin{itemize}
\item {\tt Bool.v} defines standard operations on booleans and states
and proves simple facts on them.
\item {\tt IfProp.v} defines a disjunction which contains its proof
and states its properties.
\item {\tt Zerob.v} defines the test against 0 on natural numbers and
states and proves properties of it.
\item {\tt Orb.v} states and proves facts on the boolean or.
\item {\tt DecBool.v} defines a conditional from a proof of
decidability and states its properties.
\end{itemize}
|
