@@ -482,3 +482,49 @@ runEval env e = case eval e of
482\end{SaveVerbatim}
482\end{SaveVerbatim}
483\useverb{evalexpr}
483\useverb{evalexpr}
485+\subsection{Named Instances}
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:
491+\begin{SaveVerbatim}{myord}
493+instance [myord] Ord Nat where
494+ compare O (S n) = GT
495+ compare (S n) O = LT
497+ compare (S x) (S y) = compare @{myord} x y
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:
509+\begin{SaveVerbatim}{myordlist}
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:
521+\begin{SaveVerbatim}{myordlistrun}
523+*named_instance> show (sort testList)
524+"[sO, sssO, ssssO]" : String
525+*named_instance> show (sort @{myord} testList)
526+"[ssssO, sssO, sO]" : String