Merge pull request #806 from GaloisInc/elem-type-constraints-docs

Document element type constraints for enumerations

docs/ProgrammingCryptol/crashCourse/CrashCourse.tex

@@ -446,12 +446,14 @@ constructs guarantee that enumeration elements are distinct.
   Explore various ways of constructing enumerations in Cryptol, by
   using the following expressions:
 \begin{Verbatim}
-  [1 .. 10]       // increment with step 1
-  [1, 3 .. 10]    // increment with step 2 (= 3-1)
-  [10, 9 .. 1]    // decrement with step 1 (= 10-9)
-  [10, 9 .. 20]   // decrement with step 1 (= 10-9)
-  [10, 7 .. 1]    // decrement with step 3 (= 10-7)
-  [10, 11 .. 1]   // increment with step 1
+  [1 .. 10]            // increment with step 1
+  [1, 3 .. 10]         // increment with step 2 (= 3-1)
+  [10, 9 .. 1]         // decrement with step 1 (= 10-9)
+  [10, 9 .. 20]        // decrement with step 1 (= 10-9)
+  [10, 7 .. 1]         // decrement with step 3 (= 10-7)
+  [10, 11 .. 1]        // increment with step 1
+  [1 .. 10 : [8]]      // increment 8-bit words with step 1
+  [1, 3 .. 10 : [16]]  // increment 16-bit words with step 2 (= 3-1)
 \end{Verbatim}
 \end{Exercise}
 \begin{Answer}\ansref{ex:seq:3}

docs/Syntax.md

@@ -225,6 +225,7 @@ This section provides an overview of the Cryptol's expression syntax.
     if x
       then y
       else z : Bit  // the type annotation is on `z`, not the whole `if`
+    [1..9 : [8]]    // specify that elements in `[1..9]` have type `[8]`
 
 
 **Local Declarations**