Merge requests · Iris / Iris · GitLab

Draft: Add simple library for priority levels and use it for `iFrame`

!742 · created Oct 11, 2021 by Robbert Krebbers
- 16
updated Oct 13, 2021
WIP: don't make frame_fractional an instance

!739 · created Oct 01, 2021 by Ralf Jung
- 12
updated Oct 13, 2021
Prove missing fractional_big_sepL2

!737 · created Oct 01, 2021 by Paolo G. Giarrusso
- 4
updated Oct 04, 2021
lemmas to merge a sepL and a sepL2

!735 · created Sep 11, 2021 by Ralf Jung
updated Sep 13, 2021
Extend `iInduction` with support for induction schemes containing `Forall`.

!731 · created Sep 03, 2021 by Robbert Krebbers
updated Sep 06, 2021
bi/fixpoint lemmas

!725 · created Jul 26, 2021 by Lennard Gäher
- 63
updated Oct 16, 2021
WIP: Define more uPred connectives in siProp

!710 · created Jun 29, 2021 by Hai Dang S-draft S-waiting-for-author
- 52
updated Jul 28, 2021
Formulate `is_closed_expr` in terms of `gset`s.

!707 · created Jun 20, 2021 by Dan Frumin S-waiting-for-author
- 18
updated Jul 28, 2021
move persistently_forall_2 out of BI interface

!702 · created Jun 13, 2021 by Ralf Jung S-waiting-for-review
- 18
updated Jul 28, 2021
WIP: Changing the definition of contractiveness to be compatible with Transfinite Iris

!616 · created Jan 11, 2021 by Simon Spies S-draft
- 40
updated Jul 28, 2021
Use class `IntoFUpd` in tactic `wp_value_head`

!613 · created Jan 05, 2021 by Robbert Krebbers S-waiting-for-author
- 11
updated Feb 17, 2021