Skip to content
  • 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  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  m !! j = None.
    
    That is, we have to specify the type of `m`.
    7d7c9871