-
Jean-Christophe Filliâtre authored
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
bdf87cce