 28 May, 2018 1 commit


Ralf Jung authored

 05 Apr, 2018 4 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored
This followed from discussions in https://gitlab.mpisws.org/FP/iriscoq/merge_requests/134

 31 Jan, 2018 3 commits


Robbert Krebbers authored

Robbert Krebbers authored

Robbert Krebbers authored

 14 Jan, 2018 1 commit


Robbert Krebbers authored
This is needed so that it can be used be used as a combinator for defining induction schemes for mutually inductive types.

 12 Nov, 2017 1 commit


Robbert Krebbers authored
This follows the associativity in Haskell. So, something like f <$> g <$> h Is now parsed as: (f <$> g) <$> h Since the functor is a generalized form of function application, this also now also corresponds with the associativity of function application, which is also left associative.

 09 Nov, 2017 1 commit


Robbert Krebbers authored

 28 Oct, 2017 1 commit


Robbert Krebbers authored
This way, we will be compabile with Iris's heap_lang, which puts ;; at level 100.

 24 Sep, 2017 1 commit


Robbert Krebbers authored

 21 Sep, 2017 1 commit


Robbert Krebbers authored
This allows for more control over `Hint Mode`.

 17 Sep, 2017 1 commit


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`.

 08 Sep, 2017 1 commit


Robbert Krebbers authored
See also Coq bug #5712.

 02 Sep, 2017 1 commit


Robbert Krebbers authored

 25 May, 2017 2 commits


Robbert Krebbers authored

Robbert Krebbers authored

 20 Mar, 2017 1 commit


Robbert Krebbers authored
This way, we get more definitional equalities.

 17 Mar, 2017 1 commit


Ralf Jung authored

 15 Mar, 2017 1 commit


Robbert Krebbers authored

 01 Mar, 2017 1 commit


Ralf Jung authored

 09 Feb, 2017 1 commit


Robbert Krebbers authored

 31 Jan, 2017 10 commits


Robbert Krebbers authored

Robbert Krebbers authored

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 ⊆+

Robbert Krebbers authored

Ralf Jung authored

Robbert Krebbers authored

Ralf Jung authored
This patch was created using find name *.v  xargs L 1 awk i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 ' and some minor manual editing

Robbert Krebbers authored

Robbert Krebbers authored
Also make names more consistent.

Ralf Jung authored

 09 Dec, 2016 1 commit


Ralf Jung authored

 06 Dec, 2016 1 commit


Robbert Krebbers authored

 23 Nov, 2016 1 commit


Robbert Krebbers authored

 13 Oct, 2016 1 commit


Ralf Jung authored

 20 Sep, 2016 2 commits


Robbert Krebbers authored
This also solves a name clash with the extension order of CMRAs.

Robbert Krebbers authored
