Skip to content
Snippets Groups Projects
Closed Inconsistent naming: `set_` and `_collection`
  • View options
  • Inconsistent naming: `set_` and `_collection`

  • View options
  • Closed Issue created by Robbert Krebbers

    Naming of connectives related to sets is inconsistent, e.g.:

    • set_Forall, set_Exists, set_solver, set_finite
    • seq_set
    • collection_map, collection_filter, collection_fold, collection_size, collection_equiv, collection_subseteq, collection_disjoint
    • of_option, of_list

    For finite maps, things are much more consistent: there we only use the prefix map_.

    I would like to do the same for sets, so use set_ everywhere---that's shortest and most consistent. It would mean that we have to rename at least the following:

    • set_set → set_seq
    • collection_map → set_map, collection_filter → set_filter, collection_fold → set_fold, collection_size → set_size, collection_equiv → set_equiv, collection_subseteq → set_subseteq, collection_disjoint → set_disjoint.
    • of_optionset_of_option, of_listset_of_list (which is consistent with map_of_list).

    Impact on other developments

    I don't think the impact of this will be particularly big.

    • For most of the notions, we are using operational type classes or notations anyway, i.e. we do not use the explicit names. Examples: (collection_equiv), (collection_subseteq), filter (collection_filter), ## (collection_disjoint).
    • For most of the reasoning about sets, we use set_solver.
    • All remaining renaming can easily be done by a sed script.

    Naming of the classes

    Maybe we should get rid of the whole "Collection" name altogether. This will be more invasive, since names of files will also change.

    Also, we cannot just rename the type class Collection into Set since Set is a reserved keyword.

    Class Collection A C `{ElemOf A C, Empty C, Singleton A C,
        Union C, Intersection C, Difference C} : Prop := {
      collection_simple :>> SimpleCollection A C;
      elem_of_intersection X Y (x : A) : x  X  Y  x  X  x  Y;
      elem_of_difference X Y (x : A) : x  X  Y  x  X  x  Y
    }.

    Linked items ... 0

  • Activity

    • All activity
    • Comments only
    • History only
    • Newest first
    • Oldest first
    Loading Loading Loading Loading Loading Loading Loading Loading Loading Loading