@@ -62,7 +62,7 @@ to a \texttt{String}:
6262
6363instance Show a => Show (Vect a n) where
6464 show xs = "[" ++ show' xs ++ "]" where
65− show' : Show a => Vect a n -> String
65+ show' : Vect a n' -> String
6666 show' Nil = ""
6767 show' (x :: Nil) = show x
6868 show' (x :: xs) = show x ++ ", " ++ show' xs
@@ -70,6 +70,14 @@ instance Show a => Show (Vect a n) where
7070\end{SaveVerbatim}
7171\useverb{showvec}
7272
73+\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,
79+we use a different name for the length \texttt{n'} in \texttt{show'}.
80+
7381\subsection{Default Definitions}
7482
7583The library defines an \texttt{Eq} class which provides an interface for comparing