- May 24, 2019
-
-
Hai Dang authored
-
Hai Dang authored
More consistent naming for `auth`. See merge request iris/iris!250
-
Robbert Krebbers authored
This MR is a follow up on the renamings performed (implicitly) as part of !215. This MR makes the following changes: - `auth_both_frac_valid` and `auth_both_valid` are now of the same shape as `auth_both_frac_validN` and `auth_both_validN`. That is, both are now biimplications. - The left-to-right direction of `auth_both_frac_valid` and `auth_both_valid` only holds in case the camera is discrete. The right-to-left versions for non-discrete cameras are prefixed `_2`, the convention that we use throughout the development. - Change the direction of lemmas like `auth_frag_valid` and `auth_auth_valid` so that it's consistent with the other lemmas. I.e. make sure that the ◯ and ● are always on the LHS of the biimplication.
-
- May 23, 2019
-
-
Robbert Krebbers authored
Make authoritative part of auth fractional See merge request iris/iris!215
-
-
- May 21, 2019
-
-
Robbert Krebbers authored
-
Ralf Jung authored
Make `iFresh` faster See merge request iris/iris!247
-
Ralf Jung authored
-
Ralf Jung authored
-
- May 20, 2019
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
Export that iPreProp is a Cofe See merge request iris/iris!246
-
- May 19, 2019
-
-
Robbert Krebbers authored
Generalize `iPureIntro` to support non-empty spatial contexts with just affine hypotheses. See merge request iris/iris!241
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- May 16, 2019
-
-
Paolo G. Giarrusso authored
Never used `Declare Instance`.
-
Paolo G. Giarrusso authored
-
- May 15, 2019
-
-
Ralf Jung authored
-
- May 13, 2019
-
-
Ralf Jung authored
-
- May 12, 2019
- May 09, 2019
-
-
Ralf Jung authored
-
Robbert Krebbers authored
-
- May 08, 2019
-
-
Robbert Krebbers authored
-
Ralf Jung authored
Add an `iSimpl in "%"` test. See merge request iris/iris!240
-
Ralf Jung authored
Disable new warnings for Coq master See merge request iris/iris!242
-
Tej Chajed authored
-
- May 07, 2019
-
-
Robbert Krebbers authored
-
- May 06, 2019
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Dan Frumin authored
-
- May 04, 2019
-
-
Ralf Jung authored
A more intuitive proof that lists from a COFE See merge request iris/iris!239
-
Ralf Jung authored
Add synopsis so make build-dep does not complain See merge request iris/iris!238
-
Nitpick, yes, but I've seen the complaint enough times today to bother. That complaint is only useful to maintainers, and it's even in color. ``` [WARNING] Failed checks on coq-iris-builddep package definition from source at file:///Users/pgiarrusso/git/Coq/0IRIS-SWITCH/iris/build-dep: error 57: Synopsis and description must not be both empty ```
-
Robbert Krebbers authored
This proof also more easily scales to other recursive types, like trees etc.
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
- May 02, 2019
-
-
Robbert Krebbers authored
-