@@ -53,6 +53,7 @@ Idris> show (S (S (S O)))
5353\useverb{shownat}
5454
5555\noindent
56+Only one instance of a class can be given for a type --- instances may not overlap.
5657Instance declarations can themselves have constraints. For example, to define a
5758\texttt{Show} instance for vectors, we need to know that there is a \texttt{Show}
5859instance for the element type, because we are going to use it to convert each element
@@ -71,11 +72,12 @@ instance Show a => Show (Vect a n) where
7172\useverb{showvec}
7273
7374\noindent
74−\textbf{Remark: } The type of the auxiliary function \texttt{show'} is important. The type
75−variables \texttt{a} and \texttt{n} which are part of the instance declaration for
76−\texttt{Show (Vect a n)} are fixed across the entire instance declaration. As a result,
77−we do not have to constrain \texttt{a} again. Furthermore, it means that if we use
78−\texttt{n} in the type, it refers to the length of the outermost list \texttt{xs}. Therefore,
75+\textbf{Remark: } The type of the auxiliary function \texttt{show'} is
76+important. The type variables \texttt{a} and \texttt{n} which are part of the
77+instance declaration for \texttt{Show (Vect a n)} are fixed across the entire
78+instance declaration. As a result, we do not have to constrain \texttt{a}
79+again. Furthermore, it means that if we use \texttt{n} in the type, it refers
80+to the (fixed) length of the outermost list \texttt{xs}. Therefore,
7981we use a different name for the length \texttt{n'} in \texttt{show'}.
8082
8183\subsection{Default Definitions}