The prelude function width is misleadingly named

[brianhuffman]

The name width leads users to believe (incorrectly) that the function's behavior agrees with the type-level operator of the same name. (See #549.) We should rename the value-level function to length, to match the standard list length function in common languages like Haskell, ML, etc.

Also, we need to provide a docstring for this function; currently it has none. This leads to a very confusing situation where it appears that the docstring for the type-level width applies to the value-level function as well:

Cryptol> :? width

    width : {bits, n, a} (fin n, fin bits, bits >= width n) =>
              [n]a -> [bits]

    primitive type width : # -> #

The number of bits required to represent the value of a numeric type.