• Robbert Krebbers's avatar
    Many relatively small changes. · 50dfc148
    Robbert Krebbers authored
    Most interestingly:
    * Use [lia] instead of [omega] everywhere
    * More many generic lemmas on the memory to the theory on finite maps.
    * Many additional list lemmas.
    * A new interface for a monad for collections, which is now also used by the
      collection tactics.
    * Provide an additional finite collection implementation using unordered lists
      without duplicates removed. This implementation forms a monad (just the list
      monad in disguise).
    50dfc148
nmap.v 1.97 KB