- Sep 18, 2017
- Sep 17, 2017
-
-
Robbert Krebbers authored
-
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`.
-
- Sep 08, 2017
-
-
Robbert Krebbers authored
See also Coq bug #5712.
-
- Sep 06, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Some lemmas about `difference` and `delete` See merge request !5
-
Dan Frumin authored
-
- Sep 02, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Before, we often had to insert awkward casts when using them. Also, the generality of also having them on Type, is probably not useful.
-
Robbert Krebbers authored
-
- Aug 22, 2017
- Aug 17, 2017
-
-
Robbert Krebbers authored
As suggested by Pierre-Marie Pédrot in the Coq-club thread: [Coq-Club] Very slow failing apply To work arround some performance issues in Iris.
-
Robbert Krebbers authored
-
- Aug 08, 2017
-
-
Robbert Krebbers authored
-
- Aug 02, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Jul 05, 2017
-
-
Hai Dang authored
-
- Jun 26, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- May 30, 2017
-
-
Robbert Krebbers authored
-
Dan Frumin authored
-
- May 25, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Apr 01, 2017
-
-
Robbert Krebbers authored
This is needed to use coq-stdpp in developments with -type-in-type as set_unfold will otherwise unify with any hyp, causing the set_solver tactic to break.
-
- Mar 20, 2017
-
-
Robbert Krebbers authored
This way, we get more definitional equalities.
-
- Mar 17, 2017
-
-
Ralf Jung authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-