Should we standardize on a notation for static indexing?

[satnam6502]

In #452 @blaxill defines a notation for static indexing:

Local Notation "v [@ n ]" := (indexConst v n) (at level 1, format "v [@ n ]").

I'm wary of using Notation too much. Perhaps here there is a case for using it to express static indexing? If that is the case then we should think about standardizing it across the codebase and putting it into CavaPrelude. If it was up to me I'd just use indexConst directly but I can understand that might not be popular with everyone else and the use of @ in #452 does make the indexing clearer:

    a <- xor2 (x[@0], x[@7]) ;;
    b <- xor2 (x[@2], x[@7]) ;;
    c <- xor2 (x[@3], x[@7]) ;;

What do people think? Useful enough to put in CavaPrelude?
If yes, this this the notation you'd vote for, or do you have an alternative suggestion?

[blaxill]

I'm happy to go either way, the reason for choosing this particular notation was that it matches Coq.Vector indexing style. I was initially going to do the indexing as a Coq vector, but it requires the indices are given as Fin.t. I also wasn't sure what version of indexing is preferable- in the Coq vector (after peel'ing) or via indexConst.

[jadephilipoom]

I think we should use the notation and put it in a special Notations module (maybe in CavaClass.v) that can be either imported or not depending on the implementer's preference. That way it's easy to turn the notation off if someone wants to inspect the code without it.