Thu May 9 07:26:12 EDT 2019

Random access

The point is that the primitives should support random access.  This
needs some kind of dependent typing trick to allow encoding of bounds.
If indices are not processed, this is no big deal, but I also want to
have a way to compute indices.