What is the type of the index-expression in bit-vector indexing?

[rsnikhil]

In a bit-vector index expression: v[j] : bit
what is the type of 'j'?

When I use a literal (e.g., v[7]) it works fine, but suppose j is a variable:

  let j:t = 7;
  v[j]

what should 't' be?

I've tried 'nat' and 'int' without success, probably because they are
not sufficiently constrained to be within bounds for ‘v’?

[Alasdair]

int(7) is the type of the integer 7 but here it would be better to let type inference figure it out.

In other cases you could use range<0, N> where N is the maximum index.