@@ -339,9 +339,9 @@ command at the interactive prompt.
339\label{sect:totality}
339\label{sect:totality}
341If we really want to trust our proofs, it is important that they are defined by
341If we really want to trust our proofs, it is important that they are defined by
342−\emph{total} functions --- that is, a function which is defined for all possible inputs
342+\emph{total} functions --- that is, a function which is defined for all
343−and is guaranteed to terminate. Otherwise we could construct an element of the empty type,
343+possible inputs and is guaranteed to terminate. Otherwise we could construct an
344−from which we could prove anything:
344+element of the empty type, from which we could prove anything:
346\begin{SaveVerbatim}{empties}
346\begin{SaveVerbatim}{empties}
@@ -359,8 +359,9 @@ empty2 = empty2
359\useverb{empties}
359\useverb{empties}
362−Internally, \Idris{} checks every definition for totality, and we can check at the prompt
362+Internally, \Idris{} checks every definition for totality, and we can check at
363−with the \texttt{:total} command. We see that neither of the above definitions is total:
363+the prompt with the \texttt{:total} command. We see that neither of the above
364+definitions is total:
365\begin{SaveVerbatim}{totalcheck}
366\begin{SaveVerbatim}{totalcheck}
@@ -368,16 +369,17 @@ with the \texttt{:total} command. We see that neither of the above definitions i
368possibly not total due to: empty1#hd
369possibly not total due to: empty1#hd
369 not total as there are missing cases
370 not total as there are missing cases
370*theorems> :total empty2
371*theorems> :total empty2
371−possibly not total as it is not well founded
372+possibly not total due to recursive path empty2
373\end{SaveVerbatim}
374\end{SaveVerbatim}
374\useverb{totalcheck}
375\useverb{totalcheck}
377−Note the use of the word ``possibly'' --- a totality check can, of course, never be certain
378+Note the use of the word ``possibly'' --- a totality check can, of course,
378−due to the undecidability of the halting problem. The check is, therefore, conservative.
379+never be certain due to the undecidability of the halting problem. The check
379−It is also possible (and indeed advisable, in the case of proofs) to mark functions as
380+is, therefore, conservative. It is also possible (and indeed advisable, in the
381+case of proofs) to mark functions as total so that it will be a compile time
380−total so that it will be a compile time error for the totality check to fail:
382+error for the totality check to fail:
382\begin{SaveVerbatim}{emptyfail}
384\begin{SaveVerbatim}{emptyfail}
@@ -385,7 +387,7 @@ total empty2 : _|_
385empty2 = empty2
387empty2 = empty2
387Type checking ./theorems.idr
389Type checking ./theorems.idr
388−theorems.idr:25:empty2 is possibly not total as it is not well founded
390+theorems.idr:25:empty2 is possibly not total due to recursive path empty2
390\end{SaveVerbatim}
392\end{SaveVerbatim}
391\useverb{emptyfail}
393\useverb{emptyfail}
@@ -403,15 +405,36 @@ Total
403\useverb{totdisjoint}
405\useverb{totdisjoint}
406−The totality check is currently very conservative. To be recorded as total, a function must:
408+The totality check is, necessarily, conservative. To be recorded as total, a
409+function \texttt{f} must:
408\begin{itemize}
411\begin{itemize}
409\item Cover all possible inputs
412\item Cover all possible inputs
410−\item Be \emph{well-founded} --- i.e. each recursive call must have a decreasing argument
413+\item Be \emph{well-founded} --- i.e. by the time a sequence of
411−\item Not call any non-total functions
414+(possibly mutually) recursive calls reaches \texttt{f} again, it must
415+be possible to show that one its has decreased.
412\item Not use any data types which are not \emph{strictly positive}
416\item Not use any data types which are not \emph{strictly positive}
413−\item (In version 0.9.5) Not be mutually recursive
417+\item Not call any non-total functions
420+\subsubsection{Directives and Compiler Flags for Totality}
422+By default, \Idris{} allows all definitions, whether total or not. However,
423+it is desirable for functions to be total as far as possible, as this
424+provides a guarantee that they provide a result for all possible inputs,
425+in finite time. It is possible to make total functions a requirement,
429+\item By using the \texttt{--total} compiler flag.
430+\item By adding a \texttt{\%default total} directive to a source file.
431+All definitions after this will be required to be total, unless
432+explicitly flagged as \texttt{partial}.
414\end{itemize}
433\end{itemize}
417−The last of these conditions may be relaxed in the future.
436+All functions \remph{after} a \texttt{\%default total} declaration are required
437+to be total. Correspondingly, after a \texttt{\%default partial} declaration,
438+the requirement is relaxed.