• 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
..
selection_sort_WP_SelectionSort_WP_parameter_selection_sort_1.v Loading commit data...
why3session.xml Loading commit data...