• Robbert Krebbers's avatar
    Finite maps and sets using ordered association lists. · bc659ba4
    Robbert Krebbers authored
    This commit includes the following changes:
    * More theorems about pre-, partial and total orders.
    * Define the lexicographic order on various commonly used data types.
    * Mergesort and its correctness proof.
    * Implement finite maps and sets using ordered association lists.
    bc659ba4
Name
Last commit
Last update
..
ars.v Loading commit data...
assoc.v Loading commit data...
base.v Loading commit data...
collections.v Loading commit data...
countable.v Loading commit data...
decidable.v Loading commit data...
fin_collections.v Loading commit data...
fin_map_dom.v Loading commit data...
fin_maps.v Loading commit data...
finite.v Loading commit data...
fresh_numbers.v Loading commit data...
lexico.v Loading commit data...
list.v Loading commit data...
listset.v Loading commit data...
listset_nodup.v Loading commit data...
mapset.v Loading commit data...
natmap.v Loading commit data...
nmap.v Loading commit data...
numbers.v Loading commit data...
option.v Loading commit data...
orders.v Loading commit data...
pmap.v Loading commit data...
prelude.v Loading commit data...
proof_irrel.v Loading commit data...
tactics.v Loading commit data...
vector.v Loading commit data...