summaryrefslogtreecommitdiff
path: root/theories/Logic/intro.tex
blob: 1fb294f2f58858bb4376000926f832e04f1b35f9 (plain)
1
2
3
4
5
6
7
8
\section{Logic}\label{Logic}

This library deals with classical logic and its properties.
The main file is {\tt Classical.v}.

This library also provides some facts on equalities for dependent
types. See the files {\tt Eqdep.v} and {\tt JMeq.v}.