• 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
Name
Last commit
Last update
bench Loading commit data...
doc Loading commit data...
drivers Loading commit data...
examples Loading commit data...
lib Loading commit data...
misc Loading commit data...
plugins Loading commit data...
share Loading commit data...
src Loading commit data...
stdlib Loading commit data...
tests Loading commit data...
why3-coq.opam Loading commit data...
why3-ide.opam Loading commit data...
why3.opam Loading commit data...
.dockerignore Loading commit data...
.gitattributes Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
.mailmap Loading commit data...
.merlin.in Loading commit data...
.ocp-indent Loading commit data...
AUTHORS Loading commit data...
CHANGES.md Loading commit data...
DEVELOPER.readme Loading commit data...
INSTALL.md Loading commit data...
LICENSE Loading commit data...
Makefile.in Loading commit data...
OCAML-LICENSE Loading commit data...
README.md Loading commit data...
ROADMAP Loading commit data...
TODO Loading commit data...
Version Loading commit data...
check.sh Loading commit data...
configure.in Loading commit data...