• Jean-Christophe Filliatre's avatar
    new module mach.array.ArrayInt63 for arrays of 63-bit integers · bdf87cce
    Jean-Christophe Filliatre 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
ocaml64.drv 11.2 KB