@@ -339,9 +339,9 @@ command at the interactive prompt.
339339\label{sect:totality}
340340
341341If 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
343−and is guaranteed to terminate. Otherwise we could construct an element of the empty type,
344−from which we could prove anything:
342+\emph{total} functions --- that is, a function which is defined for all
343+possible inputs and is guaranteed to terminate. Otherwise we could construct an
344+element of the empty type, from which we could prove anything:
345345
346346\begin{SaveVerbatim}{empties}
347347
@@ -359,8 +359,9 @@ empty2 = empty2
359359\useverb{empties}
360360
361361\noindent
362−Internally, \Idris{} checks every definition for totality, and we can check at the prompt
363−with the \texttt{:total} command. We see that neither of the above definitions is total:
362+Internally, \Idris{} checks every definition for totality, and we can check at
363+the prompt with the \texttt{:total} command. We see that neither of the above
364+definitions is total:
364365
365366\begin{SaveVerbatim}{totalcheck}
366367
@@ -368,16 +369,17 @@ with the \texttt{:total} command. We see that neither of the above definitions i
368369possibly not total due to: empty1#hd
369370 not total as there are missing cases
370371*theorems> :total empty2
371−possibly not total as it is not well founded
372+possibly not total due to recursive path empty2
372373
373374\end{SaveVerbatim}
374375\useverb{totalcheck}
375376
376377\noindent
377−Note the use of the word ``possibly'' --- a totality check can, of course, never be certain
378−due to the undecidability of the halting problem. The check is, therefore, conservative.
379−It is also possible (and indeed advisable, in the case of proofs) to mark functions as
380−total so that it will be a compile time error for the totality check to fail:
378+Note the use of the word ``possibly'' --- a totality check can, of course,
379+never be certain due to the undecidability of the halting problem. The check
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
382+error for the totality check to fail:
381383
382384\begin{SaveVerbatim}{emptyfail}
383385
@@ -385,7 +387,7 @@ total empty2 : _|_
385387empty2 = empty2
386388
387389Type 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
389391
390392\end{SaveVerbatim}
391393\useverb{emptyfail}
@@ -403,15 +405,36 @@ Total
403405\useverb{totdisjoint}
404406
405407\noindent
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:
407410
408411\begin{itemize}
409412\item Cover all possible inputs
410−\item Be \emph{well-founded} --- i.e. each recursive call must have a decreasing argument
411−\item Not call any non-total functions
413+\item Be \emph{well-founded} --- i.e. by the time a sequence of
414+(possibly mutually) recursive calls reaches \texttt{f} again, it must
415+be possible to show that one its has decreased.
412416\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
418+\end{itemize}
419+
420+\subsubsection{Directives and Compiler Flags for Totality}
421+
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,
426+either:
427+
428+\begin{itemize}
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}.
414433\end{itemize}
415434
416435\noindent
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.
439+
440+