1. 26 May, 2019 17 commits
  2. 25 May, 2019 17 commits
  3. 25 Apr, 2019 17 commits
  4. 20 Feb, 2019 17 commits
    • Robbert Krebbers's avatar
      Consistently use `set` and `map` names. · b7e31ce2
      Robbert Krebbers authored
      Get rid of using `Collection` and favor `set` everywhere. Also, prefer conversion
      functions that are called `X_to_Y`.
      
      The following sed script performs most of the renaming, with the exception of:
      
      - `set`, which has been renamed into `propset`. I couldn't do this rename
        using `sed` since it's too context sensitive.
      - There was a spurious rename of `Vec.of_list`, which I correctly manually.
      - Updating some section names and comments.
      
      ```
      sed '
      s/SimpleCollection/SemiSet/g;
      s/FinCollection/FinSet/g;
      s/CollectionMonad/MonadSet/g;
      s/Collection/Set\_/g;
      s/collection\_simple/set\_semi\_set/g;
      s/fin\_collection/fin\_set/g;
      s/collection\_monad\_simple/monad\_set\_semi\_set/g;
      s/collection\_equiv/set\_equiv/g;
      s/\bbset/boolset/g;
      s/mkBSet/BoolSet/g;
      s/mkSet/PropSet/g;
      s/set\_equivalence/set\_equiv\_equivalence/g;
      s/collection\_subseteq/set\_subseteq/g;
      s/collection\_disjoint/set\_disjoint/g;
      s/collection\_fold/set\_fold/g;
      s/collection\_map/set\_map/g;
      s/collection\_size/set\_size/g;
      s/collection\_filter/set\_filter/g;
      s/collection\_guard/set\_guard/g;
      s/collection\_choose/set\_choose/g;
      s/collection\_ind/set\_ind/g;
      s/collection\_wf/set\_wf/g;
      s/map\_to\_collection/map\_to\_set/g;
      s/map\_of\_collection/set\_to\_map/g;
      s/map\_of\_list/list\_to\_map/g;
      s/map\_of\_to_list/list\_to\_map\_to\_list/g;
      s/map\_to\_of\_list/map\_to\_list\_to\_map/g;
      s/\bof\_list/list\_to\_set/g;
      s/\bof\_option/option\_to\_set/g;
      s/elem\_of\_of\_list/elem\_of\_list\_to\_set/g;
      s/elem\_of\_of\_option/elem\_of\_option\_to\_set/g;
      s/collection\_not\_subset\_inv/set\_not\_subset\_inv/g;
      s/seq\_set/set\_seq/g;
      s/collections/sets/g;
      s/collection/set/g;
      ' -i $(find -name "*.v")
      ```
      b7e31ce2
  5. 29 Jan, 2019 17 commits
  6. 24 Jan, 2019 17 commits
  7. 19 Jan, 2019 17 commits
  8. 22 Nov, 2018 17 commits
  9. 06 Jun, 2018 17 commits
  10. 21 Feb, 2018 17 commits
  11. 08 Feb, 2018 17 commits
  12. 01 Nov, 2017 17 commits
    • Johannes Kloos's avatar
      Proofs of infinity and Fresh instances. · 3a262d02
      Johannes Kloos authored
      We prove that various types are infinite, notably:
      - nat, N, positive and Z;
      - string (using pretty-printing of nat);
      - option, with an infinite element type;
      - list, with an inhabited element type.
      
      Furthermore, we instantiate Fresh for strings.
      3a262d02
  13. 20 Sep, 2017 17 commits
  14. 15 Mar, 2017 17 commits
  15. 07 Feb, 2017 17 commits
  16. 06 Feb, 2017 17 commits
  17. 03 Feb, 2017 17 commits