@@ -341,12 +341,12 @@ at the \Idris{} interactive environment is shown in Figure \ref{factrun}.
341341$ idris interp.idr
342342 ____ __ _
343343 / _/___/ /____(_)____
344− / // __ / ___/ / ___/ Version 0.9.1
344+ / // __ / ___/ / ___/ Version 0.9.2
345345 _/ // /_/ / / / (__ ) http://www.idris-lang.org/
346346 /___/\__,_/_/ /_/____/ Type :? for help
347347
348348Type checking ./interp.idr
349−*interp> :exec interp
349+*interp> :exec
350350Enter a number: 6
351351720
352352*interp>
@@ -374,4 +374,38 @@ parameters at the point where the cast is applied.
374374There are casts defined between all of the primitive types, as far as
375375they make sense.
376376
377+\subsection{Unit testing}
378+
379+Recall the \texttt{so} data type:
380+
381+\useverb{sotype}
382+
383+\noindent
384+This requires its parameter to be a \texttt{True} value. One simple application of this
385+is to perform unit testing of functions at compile time. For example, we know that
386+\texttt{4! = 24} so we can set up a test case as follows:
387+
388+\begin{SaveVerbatim}{unitTestFac}
389+
390+unitTestFac : so (interp [] fact 4 == 24)
391+unitTestFac = oh
392+
393+\end{SaveVerbatim}
394+\useverb{unitTestFac}
395+
396+\noindent
397+For the program the compile, the test case must pass. If we change \texttt{24} to \texttt{25},
398+say, we will get an error message like the following:
399+
400+\begin{SaveVerbatim}{unitTestErr}
401+
402+Type checking ./interp.idr
403+interp.idr:64:Can't unify so True with so False
404+
405+Specifically:
406+ Can't unify True with False
407+
408+\end{SaveVerbatim}
409+\useverb{unitTestErr}
410+
377411