Merge Requests · Iris / Iris · GitLab

Rename `ofeT`→`ofe`, `cmraT`→`cmra`, and `ucmraT`→`ucmra`.

!623 · opened Jan 19, 2021 by Robbert
- 4
updated Jan 19, 2021
Generalize frac to dfrac in auth and view camera 0 of 1 task completed

!622 · opened Jan 16, 2021 by Simon Friis Vindum
- 10
updated Jan 19, 2021
some big_sepL lemmas

!620 · opened Jan 12, 2021 by Ralf Jung
- 23
updated Jan 19, 2021
WIP: Changing the definition of contractiveness to be compatible with Transfinite Iris

!616 · opened Jan 11, 2021 by Simon Spies
- 40
updated Jan 19, 2021
Alternative take at "better support for view shift with mismatching masks"

!615 · opened Jan 05, 2021 by Robbert
- 4
updated Jan 11, 2021
Use class `IntoFUpd` in tactic `wp_value_head`

!613 · opened Jan 05, 2021 by Robbert
- 10
updated Jan 08, 2021
add mono_nat_auth_lb

!605 · opened Dec 18, 2020 by Ralf Jung
- 7
updated Jan 07, 2021
add iris_extra package, and move view shift and Hoare triple modules into it

!602 · opened Dec 07, 2020 by Ralf Jung
- 9
updated Jan 06, 2021
Prefix iDestruct automatic names with an underscore

!599 · opened Dec 05, 2020 by Tej Chajed Iris 3.4 T-records
- 16
updated Jan 11, 2021
Add monotone resource algebra

!597 · opened Dec 02, 2020 by Amin Timany
- 13
updated Dec 10, 2020
Flexible number of logical steps per physical step 0 of 3 tasks completed

!595 · opened Nov 30, 2020 by Jacques-Henri Jourdan
- 1
- 48
updated Jan 08, 2021
Make `wp_apply` perform `wp_pure` in small steps until the lemma matches the goal.

!587 · opened Nov 12, 2020 by Robbert Iris 3.4
- 19
updated Jan 19, 2021
add big_sepS_elem_of_acc_impl

!570 · opened Nov 04, 2020 by Ralf Jung Iris 3.4
- 25
updated Jan 19, 2021
Add a verified interpreter for HeapLang

!564 · opened Nov 03, 2020 by Tej Chajed
- 30
updated Jan 05, 2021
add ghost_map library

!562 · opened Nov 02, 2020 by Ralf Jung
- 15
updated Dec 14, 2020
better support for view shift with mismatching masks

!527 · opened Oct 02, 2020 by Ralf Jung S-waiting-for-review
- 2
updated Jan 11, 2021
Define logic `clProp` for axiom-free classical logic + remove `pure_forall_2` from BI interface

!496 · opened Sep 05, 2020 by Robbert S-blocked
- 39
updated Dec 09, 2020
Support destructing exists with intro patterns

!483 · opened Jul 22, 2020 by Tej Chajed S-waiting-for-review T-records
- 13
updated Dec 23, 2020
WIP: Prepend introduction pattern `H.ipat`. 0 of 1 task completed

!480 · opened Jul 19, 2020 by Robbert S-blocked T-records
- 22
updated Nov 06, 2020
WIP: Remove `contractive_ne` and `contractive_proper` as instances.

!455 · opened May 27, 2020 by Robbert S-waiting-for-author
- 12
updated Nov 06, 2020