• Robbert Krebbers's avatar
    Various minor changes. · 4cda26dd
    Robbert Krebbers authored
    * Introduce a type class and notation for disjointness.
    * Define unions of finite maps (a lot of theory has still to be
      moved from memory to fin_maps).
    * Prove the Hoare rule for function calls with arguments.
    * Prove the Hoare rule to add sets of functions.
    * Some additional theory on lifting of assertions.
    4cda26dd
fin_maps.v 18.5 KB