@@ -482,3 +482,49 @@ runEval env e = case eval e of
482482\end{SaveVerbatim}
483483\useverb{evalexpr}
484484
485+\subsection{Named Instances}
486+
487+It can be desirable to have multiple instances of a type class, for example to provide
488+alternative methods for sorting or printing values. To achieve this, instances can
489+be \remph{named} as follows:
490+
491+\begin{SaveVerbatim}{myord}
492+
493+instance [myord] Ord Nat where
494+ compare O (S n) = GT
495+ compare (S n) O = LT
496+ compare O O = EQ
497+ compare (S x) (S y) = compare @{myord} x y
498+
499+\end{SaveVerbatim}
500+\useverb{myord}
501+
502+\noindent
503+This declares an instance as normal, but with an explicit name, \texttt{myord}.
504+The syntax \texttt{compare @\{myord\}} gives an explicit instance to
505+\texttt{compare}, otherwise it would use the default instance for \texttt{Nat}.
506+We can use this, for example, to sort a list of \texttt{Nat}s in reverse.
507+Given the following list:
508+
509+\begin{SaveVerbatim}{myordlist}
510+
511+testList : List Nat
512+testList = [3,4,1]
513+
514+\end{SaveVerbatim}
515+\useverb{myordlist}
516+
517+\noindent
518+\ldots we can sort it using the default \texttt{Ord} instance, then the named
519+instance \texttt{myord} as follows, at the \Idris{} prompt:
520+
521+\begin{SaveVerbatim}{myordlistrun}
522+
523+*named_instance> show (sort testList)
524+"[sO, sssO, ssssO]" : String
525+*named_instance> show (sort @{myord} testList)
526+"[ssssO, sssO, sO]" : String
527+
528+\end{SaveVerbatim}
529+\useverb{myordlist}
530+