• 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
..
algebra.why Loading commit data...
bag.why Loading commit data...
bintree.why Loading commit data...
bool.why Loading commit data...
comparison.why Loading commit data...
floating_point.why Loading commit data...
function.why Loading commit data...
graph.why Loading commit data...
int.why Loading commit data...
list.why Loading commit data...
map.why Loading commit data...
number.why Loading commit data...
option.why Loading commit data...
pigeon.why Loading commit data...
real.why Loading commit data...
regexp.why Loading commit data...
relations.why Loading commit data...
set.why Loading commit data...
sum.why Loading commit data...
tptp.why Loading commit data...