@@ -62,7 +62,7 @@ to a \texttt{String}:
63instance Show a => Show (Vect a n) where
63instance Show a => Show (Vect a n) where
64 show xs = "[" ++ show' xs ++ "]" where
64 show xs = "[" ++ show' xs ++ "]" where
65− show' : Show a => Vect a n -> String
65+ show' : Vect a n' -> String
66 show' Nil = ""
66 show' Nil = ""
67 show' (x :: Nil) = show x
67 show' (x :: Nil) = show x
68 show' (x :: xs) = show x ++ ", " ++ show' xs
68 show' (x :: xs) = show x ++ ", " ++ show' xs
@@ -70,6 +70,14 @@ instance Show a => Show (Vect a n) where
70\end{SaveVerbatim}
70\end{SaveVerbatim}
71\useverb{showvec}
71\useverb{showvec}
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'}.
73\subsection{Default Definitions}
81\subsection{Default Definitions}
75The library defines an \texttt{Eq} class which provides an interface for comparing
83The library defines an \texttt{Eq} class which provides an interface for comparing