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