# Array access in transformations with arguments

In transformation with arguments, stuff defined with a notation cannot be reused if the notation is overloaded.

In Array63 module we have:
`function ([]) (a: array 'a) (i: int) : 'a = a.elts i`

And an example is:

```
module Test
use import array.Array
use import mach.array.Array63
constant d: Array.array int
constant e: Array63.array int
goal a: e[1] = 5
goal c: Array.([]) d 3 = 5
end
```

In the above, notation [] cannot be used for array d as the notation [] is used for Array63. In this example, it is not even possible to talk about Array.([]) in transformations.

The complete solution would be to accept qualified expressions in arguments of tactics: this may be difficult.

I think it's possible to disambiguate the mixfix notation as we do for infix (==^ ==^^ etc). It would require to extend the parser a little so that "[ term ]", "[ ^ term ]", "[ ^ ^ term ]" are recognized (or any similar notation).

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information