Skip to content
Snippets Groups Projects
  1. Oct 10, 2017
  2. Oct 09, 2017
  3. Oct 07, 2017
  4. Oct 06, 2017
  5. Sep 29, 2017
  6. Sep 28, 2017
  7. Sep 27, 2017
  8. Sep 26, 2017
  9. Sep 24, 2017
  10. Sep 21, 2017
  11. Sep 20, 2017
  12. Sep 18, 2017
  13. Sep 17, 2017
    • Robbert Krebbers's avatar
      b371f874
    • Robbert Krebbers's avatar
      Set Hint Mode for all classes in `base.v`. · 7d7c9871
      Robbert Krebbers authored
      This provides significant robustness against looping type class search.
      
      As a consequence, at many places throughout the library we had to add
      additional typing information to lemmas. This was to be expected, since
      most of the old lemmas were ambiguous. For example:
      
        Section fin_collection.
          Context `{FinCollection A C}.
      
          size_singleton (x : A) : size {[ x ]} = 1.
      
      In this case, the lemma does not tell us which `FinCollection` with
      elements `A` we are talking about. So, `{[ x ]}` could not only refer to
      the singleton operation of the `FinCollection A C` in the section, but
      also to any other `FinCollection` in the development. To make this lemma
      unambigious, it should be written as:
      
        Lemma size_singleton (x : A) : size ({[ x ]} : C) = 1.
      
      In similar spirit, lemmas like the one below were also ambiguous:
      
        Lemma lookup_alter_None {A} (f : A → A) m i j :
          alter f i m !! j = None :left_right_arrow: m !! j = None.
      
      It is not clear which finite map implementation we are talking about.
      To make this lemma unambigious, it should be written as:
      
        Lemma lookup_alter_None {A} (f : A → A) (m : M A) i j :
          alter f i m !! j = None :left_right_arrow: m !! j = None.
      
      That is, we have to specify the type of `m`.
      7d7c9871
  14. Sep 08, 2017
  15. Sep 06, 2017
Loading