Merge Requests · Iris / Iris · GitLab

Make `_iff` and `_alter` lemmas for invariants consistent, and add `_iff` lemma for locks

!414 · opened Apr 01, 2020 by Robbert
- 2
updated Apr 01, 2020
Kill `{o,r,ur}Functor_diag` coercions, and rename into `{o,r,ur}Functor_apply`

!413 · opened Apr 01, 2020 by Robbert
- 18
updated Apr 01, 2020
Notion of composition on `oFunctor`s, and some renaming

!411 · opened Mar 31, 2020 by Robbert
- 9
updated Apr 01, 2020
WIP: Fix notation issues in #302

!409 · opened Mar 31, 2020 by Paolo G. Giarrusso
- 14
updated Mar 31, 2020
make direction and names of more `f_op`/`f_core` rewrite lemmas more consistent

!403 · opened Mar 27, 2020 by Ralf Jung
- 9
updated Mar 31, 2020
Add support for pure names in intro patterns

!400 · opened Mar 23, 2020 by Tej Chajed Iris 3.3
- 2
- 62
updated Apr 01, 2020
ASCII notation

!396 · opened Mar 18, 2020 by Gregory Malecha Iris 3.3
- 110
updated Apr 02, 2020
WIP: Generic union, disjoint union CMRAs for sets.

!381 · opened Feb 23, 2020 by David Swasey S-waiting-for-author
- 1
- 28
updated Apr 01, 2020
WIP: Add lemmas about local updates of lists

!371 · opened Feb 06, 2020 by Dmitry Khalanskiy S-waiting-for-author
- 35
updated Mar 20, 2020
Implement CMRA via an isomorphism to another CMRA

!348 · opened Dec 15, 2019 by Tej Chajed
- 16
updated Mar 27, 2020
WIP: Documentation on Iris equalities

!300 · opened Aug 09, 2019 by Paolo G. Giarrusso S-waiting-for-author
- 63
updated Mar 31, 2020
Add heap_lang lib for "GC locations": locations that can never be deallocated

!289 · opened Jul 12, 2019 by Ralf Jung Iris 3.3 S-waiting-for-review
- 32
updated Mar 27, 2020
WIP: Make `[#]` produce goal with `<pers>` modality if premise is not persistent

!216 · opened Feb 17, 2019 by Dan Frumin Iris 3.3 S-waiting-for-review
- 10
updated Apr 01, 2020