summaryrefslogtreecommitdiff
path: root/theories/Reals/intro.tex
blob: 433172585bb1696daa559d388a3176bad63a0edc (plain)
1
2
3
4
\section{Reals}\label{Reals}

This library contains an axiomatization of real numbers.
The main file is \texttt{Reals.v}.