• 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
numbers.v 16 KB