the model is a sequence of integers, of type 'seq int'
the idea is to lower the pollution of VCs with values of int63 (and
subsequent to_int operations)
drawbacks:
- this new type of arrays is not compatible with the one
from mach.array.Array63
- when using both, we cannot use syntax [] and []<- for both types
in programs (no overloading in programs) and thus we have to use
A.([]) and A.([]<-) for one of them
instead of a function of type int->'a
a coercion is declared from arrays to sequences, so that notation a[i]
in the logic now refers to the sequence operation
small caveat: you have to open module seq.Seq to be able to use this
notation
