Merge Requests · Iris · GitLab

WIP: Add Michael Scott queue

reloc!4 · opened Jun 05, 2020 by Simon Friis Vindum
updated Sep 10, 2020
Draft: use SProp for well-formedness condition in Pmap and gmap

stdpp!189 · opened Oct 05, 2020 by Tej Chajed
- 3
updated Oct 07, 2020
WIP: Prepend introduction pattern `H.ipat`. 0 of 1 task completed

iris!480 · opened Jul 19, 2020 by Robbert Krebbers S-blocked T-records
- 22
updated Nov 06, 2020
WIP: Changing the definition of contractiveness to be compatible with Transfinite Iris

iris!616 · opened Jan 11, 2021 by Simon Spies
- 40
updated Jan 28, 2021
Support destructing exists with intro patterns

iris!483 · opened Jul 22, 2020 by Tej Chajed S-blocked T-records
- 13
updated Feb 01, 2021
FromPure instances for big_sepM

iris!626 · opened Jan 27, 2021 by Ralf Jung
- 5
updated Feb 01, 2021
Define logic `clProp` for axiom-free classical logic + remove `pure_forall_2` from BI interface

iris!496 · opened Sep 05, 2020 by Robbert Krebbers S-blocked
- 40
updated Feb 03, 2021
Add monotone resource algebra

iris!597 · opened Dec 02, 2020 by Amin Timany
- 14
updated Feb 03, 2021
Use the persistent function space in logical relations and add the symbol table example

examples!38 · opened Jun 11, 2020 by Amin Timany
- 42
updated Feb 03, 2021
Alternative take at "better support for view shift with mismatching masks"

iris!615 · opened Jan 05, 2021 by Robbert Krebbers S-waiting-for-author
- 5
updated Feb 13, 2021
Prefix iDestruct automatic names with an underscore

iris!599 · opened Dec 05, 2020 by Tej Chajed S-blocked T-records
- 19
updated Feb 15, 2021
Add lemmas about local updates of lists

iris!371 · opened Feb 06, 2020 by Dmitry Khalanskiy S-waiting-for-review
updated Feb 15, 2021
Provide functionality from string_ident natively

iris!640 · opened Feb 15, 2021 by Tej Chajed
- 8
updated Feb 16, 2021
better support for view shift with mismatching masks

iris!527 · opened Oct 02, 2020 by Ralf Jung S-waiting-for-review
- 11
updated Feb 17, 2021
Use class `IntoFUpd` in tactic `wp_value_head`

iris!613 · opened Jan 05, 2021 by Robbert Krebbers S-waiting-for-author
- 11
updated Feb 17, 2021
add ghost_map library

iris!562 · opened Nov 02, 2020 by Ralf Jung S-waiting-for-review
- 17
updated Feb 17, 2021
Add a verified interpreter for HeapLang

iris!564 · opened Nov 03, 2020 by Tej Chajed S-waiting-for-review
- 41
updated Feb 18, 2021
Draft: Case study: page table

refinedc!42 · opened Feb 19, 2021 by Fengmin Zhu
- 0
updated Feb 25, 2021
Enable `Typeclasses Strict Resolution` for dervied_connectives.v 0 of 1 task completed

iris!642 · opened Feb 19, 2021 by Janno
- 5
updated Feb 28, 2021
register make_laterable as modality

iris!636 · opened Feb 12, 2021 by Ralf Jung
- 1
updated Mar 03, 2021