update documentation for #82

docs/CryptolPrims.md

@@ -158,9 +158,9 @@ New types:
     // Abbreviations
     splitBy n = split`{parts = n}
     groupBy n = split`{each  = n}
-    tail n    = splitAt`{front = 1}.2
-    take n    = splitAt`{front = n}.1
-    drop n    = splitAt`{front = n}.2
+    tail n    = splitAt`{front = 1}.1
+    take n    = splitAt`{front = n}.0
+    drop n    = splitAt`{front = n}.1
 
     /* Also, `length` is not really needed:
        length : {n,a,m} (m >= width n) => [n]a -> [m]

docs/ProgrammingCryptol/appendices/Syntax.tex

@@ -227,8 +227,8 @@ pattern matching or by using explicit component selectors. Explicit
 component selectors are written as follows:
 
 \begin{verbatim}
-(15, 20).1           == 15
-(15, 20).2           == 20
+(15, 20).0           == 15
+(15, 20).1           == 20
 
 { x = 15, y = 20 }.x == 15
 \end{verbatim}

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -238,15 +238,15 @@ Here are Cryptol's responses:
   semantics at the object level in different contexts.}
 
 \paragraph*{Projecting values from tuples} Use a {\tt .} followed by
-$n$ to project the $n$-th component of a tuple.  Nested projection is
+$n$ to project the $n+1$-th component of a tuple.  Nested projection is
 not supported at this time.
 
 \begin{Exercise}\label{ex:tup:2}
 Try out the following examples:
 \begin{Verbatim}
+  (1, 2+4).0
   (1, 2+4).1
-  (1, 2+4).2
-  ((1, 2), False, (3-1, (4, True))).3
+  ((1, 2), False, (3-1, (4, True))).2
 \end{Verbatim}
 \todo[inline]{Include a more interesting nested example here once
   \href{https://www.galois.com/cryptol/ticket/220}{ticket \#220} is
@@ -259,16 +259,16 @@ projection to extract the value {\tt False} from the expression:
 \begin{Answer}\ansref{ex:tup:2}
 Here are Cryptol's responses:
 \begin{Verbatim}
-  Cryptol> (1, 2+4).1
+  Cryptol> (1, 2+4).0
   1
-  Cryptol> (1, 2+4).2
+  Cryptol> (1, 2+4).1
   6
-  Cryptol> ((1, 2), False, (3-1, (4, True))).3
+  Cryptol> ((1, 2), False, (3-1, (4, True))).2
   (2, (4, True))
 \end{Verbatim}
 The required expression would be:
 \begin{Verbatim}
-  ((1, 2), (2, (4, True), 6), False).3
+  ((1, 2), (2, (4, True), 6), False).2
 \end{Verbatim}
 \end{Answer}
 
@@ -1161,8 +1161,8 @@ In Cryptol, records are simply collections of named fields. In this
 sense, they are very similar to tuples (Section~\ref{sec:tuple}),
 which can be thought of records without field names\footnote{In fact,
   the fields of a tuple {\it can} be accessed via the dot-notation,
-  with their names being their 1-indexed position in the tuple. So
-  {\tt (1,2).2 == 2}.}. Like a tuple, the fields of a record can be of
+  with their names being their 0-indexed position in the tuple. So
+  {\tt (1,2).1 == 2}.}. Like a tuple, the fields of a record can be of
 any type.  We construct records by listing the fields inside
 curly-braces, separated by commas.  We project fields out of a record
 with the usual dot-notation.  Note that the order of fields in a
@@ -1594,7 +1594,7 @@ in parentheses, separated by commas: {\tt (3, 5, True) : ([8], [32],
   Bit)}. Tuples' types follow the same structure: {\tt (2, (False, 3),
   5) : ([8], (Bit, [32]), [32])}.  A tuple component can be any type:
 a word, another tuple, sequence, record, etc. Again, type inference
-makes writing tuple types hardly every necessary.\indTypeInference
+makes writing tuple types hardly ever necessary.\indTypeInference
 
 \paragraph*{Sequences}\indTheSequenceType A sequence is simply a 
 collection of homogeneous elements. If the element type is {\tt t},

docs/Syntax.md

@@ -213,8 +213,8 @@ The components of a record or a tuple may be accessed in two ways: via
 pattern matching or by using explicit component selectors.  Explicit
 component selectors are written as follows:
 
-    (15, 20).1           == 15
-    (15, 20).2           == 20
+    (15, 20).0           == 15
+    (15, 20).1           == 20
 
     { x = 15, y = 20 }.x == 15