From 7b0b8836c0d3e59d3032b35855808f0f5f93774d Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 5 Oct 2017 10:20:57 -0700 Subject: [PATCH] Fix outdated reference to `inf a` constraint in docs. --- docs/ProgrammingCryptol/crashCourse/CrashCourse.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex index 231dfb28..7cbd47a4 100644 --- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex +++ b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex @@ -1841,9 +1841,9 @@ In general, type predicates exclusively describe \textit{arithmetic constraints on type variables}. Cryptol does not have a general-purpose dependent type system, but a \emph{size-polymorphic type system}. Often type variables' values are of finite size, -indicated with the constraint {\tt fin a}\indFin, otherwise no -constraint is mentioned or an explicit \texttt{inf a} is -denoted\indInf, and the variables' values are unbounded. Arithmetic +indicated with the constraint {\tt fin a}\indFin; otherwise no +constraint is mentioned, and the variables' values are unbounded, +possibly taking the value \texttt{inf}\indInf. Arithmetic relations are arbitrary relations over all type variables, such as {\tt 2*a+b >= c}. We shall see more examples as we work through programs later on.