aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool/intro.tex
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}