Update documenetation with new enumeration forms

CHANGES.md

@@ -9,6 +9,12 @@
       convenient when writing `private` declarations as they don't need to
       be indented as long as they are at the end of the file.
 
+* New enumeration forms `[x .. y by n]`, `[x .. <y by n]`,
+  `[x .. y down by n]` and `[x .. >y down by n]` have been
+  implemented. These new forms let the user explicitly specify
+  the stride for an enumeration, as opposed to the previous
+  `[x, y .. z]` form (where the stride was computed from `x` and `y`).
+
 ## New features
 
 * What4 prover backends now feature an improved multi-SAT procedure

docs/CryptolPrims.md

@@ -25,24 +25,51 @@ Literals
     number : {val, rep} Literal val rep => rep
     length : {n, a, b} (fin n, Literal n b) => [n]a -> b
 
-    // '[a..b]' is syntactic sugar for 'fromTo`{first=a,last=b}'
+    // '[x..y]' is syntactic sugar for 'fromTo`{first=x,last=y}'
     fromTo : {first, last, a}
                (fin last, last >= first,
                Literal first a, Literal last a) =>
                [1 + (last - first)]a
 
-    // '[a,b..c]' is syntactic sugar for 'fromThenTo`{first=a,next=b,last=c}'
+    // '[x .. < y]' is syntactic sugar for
+    //   'fromToLessThan`{first=x,bound=y}'
+    fromToLessThan : {first, bound, a}
+         (fin first, bound >= first, LiteralLessThan bound a) =>
+         [bound - first]a
+
+    // '[x,y..z]' is syntactic sugar for
+    //   'fromThenTo`{first=x,next=y,last=z}'
     fromThenTo : {first, next, last, a, len}
                    ( fin first, fin next, fin last
                    , Literal first a, Literal next a, Literal last a
                    , first != next
                    , lengthFromThenTo first next last == len) =>
                   [len]a
 
-    // '[a .. < b]` is syntactic sugar for 'fromToLessThan`{first=a,bound=b}'
-    fromToLessThan : {first, bound, a}
-         (fin first, bound >= first, LiteralLessThan bound a) =>
-         [bound - first]a
+    // '[x .. y by n]' is syntactic sugar for
+    //    'fromToBy`{first=x,last=y,stride=n}'.
+    primitive fromToBy : {first, last, stride, a}
+      (fin last, fin stride, stride >= 1, last >= first, Literal last a) =>
+      [1 + (last - first)/stride]a
+
+    // '[x ..< y by n]' is syntactic sugar for
+    //   'fromToByLessThan`{first=x,bound=y,stride=n}'.
+    primitive fromToByLessThan : {first, bound, stride, a}
+      (fin first, fin stride, stride >= 1, bound >= first, LiteralLessThan bound a) =>
+      [(bound - first)/^stride]a
+
+    // '[x .. y down by n]' is syntactic sugar for
+    //   'fromToDownBy`{first=x,last=y,stride=n}'.
+    primitive fromToDownBy : {first, last, stride, a}
+      (fin first, fin stride, stride >= 1, first >= last, Literal first a) =>
+      [1 + (first - last)/stride]a
+
+    // '[x ..> y down by n]' is syntactic sugar for
+    //   'fromToDownByGreaterThan`{first=x,bound=y,stride=n}'.
+    primitive fromToDownByGreaterThan : {first, bound, stride, a}
+      (fin first, fin stride, stride >= 1, first >= bound, Literal first a) =>
+      [(first - bound)/^stride]a
+
 
 Fractional Literals
 -------------------