• 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
tactics.v 24 KB