Update the Cryptol documentation with the new 'update' primitives

docs/CryptolPrims.md

@@ -67,11 +67,14 @@ Sequences
     reverse   : {n,a} (fin n) => [n]a -> [n]a
     transpose : {n,m,a} [n][m]a -> [m][n]a
 
-    (@)        : {n a m}              [n]a -> [m]    -> a
-    (@@)       : {n a m i}            [n]a -> [m][i] -> [m]a
-    (!)        : {n a m}   (fin n) => [n]a -> [m]    -> a
-    (!!)       : {n a m i} (fin n) => [n]a -> [m][i] -> [m]a
-
+    (@)        : {n,a,m}              [n]a -> [m]    -> a
+    (@@)       : {n,a,m,i}            [n]a -> [m][i] -> [m]a
+    (!)        : {n,a,m}   (fin n) => [n]a -> [m]    -> a
+    (!!)       : {n,a,m,i} (fin n) => [n]a -> [m][i] -> [m]a
+    update     : {n,a,m} (fin m) => [n]a -> [m] -> a -> [n]a
+    updateEnd  : {n,a,m} (fin n, fin m) => [n]a -> [m] -> a -> [n]a
+    updates    : {n,a,m,d} (fin m, fin d) => [n]a -> [d]([m], a) -> [n]a
+    updatesEnd : {n,a,m,d} (fin n, fin m, fin d) => [n]a -> [d]([m], a) -> [n]a
 
     // Abbreviations
     groupBy n = split`{each  = n}

docs/ProgrammingCryptol/prims/Primitives.tex

@@ -49,6 +49,10 @@ primsPlaceHolder=1;
     !       : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b
     @@      : {a, b, c, d} (fin d) => [a]b -> [c][d] -> [c]b
     !!      : {a, b, c, d} (fin a, fin d) => [a]b -> [c][d] -> [c]b
+    update     : {a, b, c} (fin c) => [a]b -> [c] -> b -> [a]b
+    updateEnd  : {a, b, c} (fin a, fin c) => [a]b -> [c] -> b -> [a]b
+    updates    : {a,b,c,d} (fin c, fin d) => [a]b -> [d]([c], b) -> [a]b
+    updatesEnd : {a,b,c,d} (fin a, fin c, fin d) => [a]b -> [d]([c], b) -> [a]b
     width   : {bits,len,elem} (fin len, fin bits, bits >= width len)
            => [len] elem -> [bits]
 \end{Verbatim}

docs/Syntax.md

@@ -271,13 +271,15 @@ Note: the bounds in finite unbounded (those with ..) sequences are
 type expressions, while the bounds in bounded-finite and infinite
 sequences are value expressions.
 
-Operator        Description
---------        -----------
-  `#`           Sequence concatenation
-  `>>`  `<<`    Shift (right,left)
-  `>>>` `<<<`   Rotate (right,left)
-  `@` `!`       Access elements (front,back)
-  `@@` `!!`     Access sub-sequence (front,back)
+Operator                       Description
+---------------------------    -----------
+  `#`                          Sequence concatenation
+  `>>`  `<<`                   Shift (right,left)
+  `>>>` `<<<`                  Rotate (right,left)
+  `@` `!`                      Access elements (front,back)
+  `@@` `!!`                    Access sub-sequence (front,back)
+  `update` `updateEnd`         Update the value of a sequence at a location (front,back)
+  `updates` `updatesEnd`       Update multiple values of a sequence (front,back)
 
 Table: Sequence operations.