From 70180fd4c9b82581fe9de2b54320497ae90a5139 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 22 Sep 2020 18:09:20 -0700 Subject: [PATCH] Fix wrong inferred type for `twoPlusXY` in book exercise. Fixes #887. --- docs/ProgrammingCryptol/crashCourse/CrashCourse.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex index 64cfdb833..b575a690a 100644 --- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex +++ b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex @@ -2255,12 +2255,12 @@ \subsection{Local names: {\ttfamily{\textbf where}} clauses} Here is the type Cryptol infers: \begin{verbatim} Cryptol> :t twoPlusXY - twoPlusXY : {a} (a >= 2, fin a) => ([a],[a]) -> [a] + twoPlusXY : {a} (Ring a, Literal 2 a) => (a, a) -> a \end{verbatim} -That is, our function will actually work over arbitrary (finite) sized -words, as long as they are at least 2 bits wide. The 2-bit requirement -comes from the constant 2, which requires at least 2 bits to -represent. +That is, our function will actually work over an arbitrary ring, as +long as it is large enough to represent the literal 2. The +\texttt{Ring} and \texttt{Literal} type constraints are discussed +further in \autoref{sec:type-classes}. \end{Answer} \todo[inline]{The Cmp class has not been introduced yet. At least, add a forward reference to the ``Type classes'' section.}