From 505eb0f0dae9b8a6ac810070d60916b67942b305 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 31 Jul 2015 09:34:48 +0200 Subject: Remove some outdated files and fix permissions. --- theories/Arith/intro.tex | 55 ------------------------------------------------ 1 file changed, 55 deletions(-) delete mode 100755 theories/Arith/intro.tex (limited to 'theories/Arith') diff --git a/theories/Arith/intro.tex b/theories/Arith/intro.tex deleted file mode 100755 index 655de34ca..000000000 --- a/theories/Arith/intro.tex +++ /dev/null @@ -1,55 +0,0 @@ -\section{Arith}\label{Arith} - -The {\tt Arith} library deals with various arithmetical notions and -their properties. - -\subsection*{Standard {\tt Arith} library} - -The following files are automatically loaded by {\tt Require Arith}. - -\begin{itemize} - -\item {\tt Le.v} states and proves properties of the large order {\tt le}. - -\item {\tt Lt.v} states and proves properties of the strict order {\tt -lt} (especially, the relationship with {\tt le}). - -\item {\tt Plus.v} states and proves properties on the addition. - -\item {\tt Gt.v} states and proves properties on the strict order {\tt gt}. - -\item {\tt Minus.v} defines the difference on -{\tt nat} and proves properties of it. On {\tt nat}, {\tt (minus n p)} is -{\tt O} if {\tt n} $<$ {\tt p}. - -\item {\tt Mult.v} states and proves properties on the multiplication. - -\item {\tt Between.v} defines modalities on {\tt nat} and proves properties -of them. - -\end{itemize} - -\subsection*{Additional {\tt Arith} library} - -\begin{itemize} - -\item {\tt Compare.v}, {\tt Compare\_dec.v} and {\tt Peano\_dec.v} state -and prove various decidability results on {\tt nat}. - -\item {\tt Wf\_nat.v} states and proves various induction and recursion -principles on {\tt nat}. Especially, recursion for objects measurable by -a natural number and recursion on {\tt nat * nat} are provided. - -\item {\tt Min.v} defines the minimum of two natural numbers and proves -properties of it. - -\item {\tt Eqnat.v} defines a specific equality on {\tt nat} and shows -the equivalence with Leibniz' equality. - -\item {\tt Euclid.v} proves that the euclidean -division specification is realisable. Conversely, {\tt Div.v} exhibits -two different algorithms and semi-automatically reconstruct the proof of -their correctness. These files emphasize the extraction of program vs -reconstruction of proofs paradigm. - -\end{itemize} -- cgit v1.2.3