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).