• 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
algo65.mlw 1.75 KB