• Jean-Christophe Filliatre's avatar
    library: map.MapPermut now defined using map.Occ · ca0ec4aa
    Jean-Christophe Filliatre authored
    (that is, using number of occurrences)
    No more definition of permutation using inductive predicates.
    Impacts array.ArrayPermut; proof sessions updated.
    Coq realizations for map.Occ and map.MapPermut;
    proof session for array.ArrayPermut in progress
    ca0ec4aa
Name
Last commit
Last update
bench Loading commit data...
bin Loading commit data...
comparison Loading commit data...
doc Loading commit data...
drivers Loading commit data...
examples Loading commit data...
lib Loading commit data...
misc Loading commit data...
modules Loading commit data...
plugins Loading commit data...
share Loading commit data...
src Loading commit data...
tests Loading commit data...
theories Loading commit data...
.gitignore Loading commit data...
AUTHORS Loading commit data...
CHANGES Loading commit data...
DEVELOPER.readme Loading commit data...
INSTALL Loading commit data...
LICENSE Loading commit data...
Makefile.in Loading commit data...
OCAML-LICENSE Loading commit data...
README 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...