Skip to content
Snippets Groups Projects
Forked from Iris / Iris
Source project has a limited visibility.
  • Robbert Krebbers's avatar
    ddf8ef49
    Renaming in prelude/list. · ddf8ef49
    Robbert Krebbers authored
    Rename:
    
    - prefix_of -> prefix and suffix_of -> suffix because that saves keystrokes
      in lemma names. However, keep the infix notations with l1 `prefix_of` l2 and
      l1 `suffix_of` l2 because those are easier to read.
    - change the notation l1 `sublist` l2 into l1 `sublist_of` l2 to be consistent.
    - rename contains -> submseteq and use the notation ⊆+
    ddf8ef49
    History
    Renaming in prelude/list.
    Robbert Krebbers authored
    Rename:
    
    - prefix_of -> prefix and suffix_of -> suffix because that saves keystrokes
      in lemma names. However, keep the infix notations with l1 `prefix_of` l2 and
      l1 `suffix_of` l2 because those are easier to read.
    - change the notation l1 `sublist` l2 into l1 `sublist_of` l2 to be consistent.
    - rename contains -> submseteq and use the notation ⊆+