Merge requests · Iris / Iris · GitLab

fix forgotten rename: head_redex -> base_redex

!1024 · created Dec 05, 2023 by Ralf Jung
- 1
updated Dec 05, 2023
Refactor proofs of {impl,wand}_timeless

!1023 · created Dec 02, 2023 by Johannes Hostert
- 27
updated Dec 06, 2023
Do not use eta-expansion in `into_forall_forall`.

!1020 · created Nov 15, 2023 by Robbert Krebbers
- 4
updated Dec 02, 2023
Improve `iFrame` to instantiate existential quantifiers

!1017 · created Nov 10, 2023 by Ike Mulder
- 29
updated Nov 18, 2023
More documentation about _1 and _2 lemmas.

!1008 · created Oct 18, 2023 by Robbert Krebbers
- 2
updated Oct 20, 2023
Add notations for `<affine> ⌜ ⌝` and friends.

!1007 · created Oct 15, 2023 by Robbert Krebbers
- 12
updated Oct 17, 2023
Add `IsOp` instances for `gset`, `coPset`, `gmultiset`

!1004 · created Oct 11, 2023 by Ike Mulder
- 5
updated Nov 10, 2023
Draft: Make sure that `?` in `iIntros`/`iDestruct` generate names that are not in the pattern

!992 · created Oct 03, 2023 by Robbert Krebbers
- 9
updated Oct 04, 2023
Avoid using specific `G` classes for locks, always use the projection `lockG` of `lock`.

!980 · created Aug 29, 2023 by Robbert Krebbers
updated Aug 30, 2023
Draft: experiment: use coq's ability to infer more canonical structures

!972 · created Aug 11, 2023 by Ralf Jung
S-blocked
updated Aug 28, 2023
Draft: Attempted fix for #539, solving slow type-checking of nested `●` terms

!971 · created Aug 10, 2023 by Ike Mulder
updated Aug 28, 2023
generalize gmap_view for an arbitrary CMRA as values

!959 · created Jul 27, 2023 by Ralf Jung
S-waiting-for-review
- 27
updated Dec 05, 2023
Draft: Avoid `Local Ltac` and `Local Tactic Notation` in proofmode.

!953 · created Jul 24, 2023 by Robbert Krebbers
updated Aug 05, 2023
Make bi fields non-canonical

!933 · created May 26, 2023 by Paolo G. Giarrusso
S-blocked
updated Oct 13, 2023
Draft: Improve validity information received from `iCombine`ing `own`s

!930 · created May 25, 2023 by Ike Mulder
updated Nov 10, 2023
`Unify` type class that factors out use of `notypeclasses refine` in proof mode classes.

!916 · created Apr 30, 2023 by Robbert Krebbers
S-waiting-for-author
- 6
updated Jul 25, 2023
add fixpoint lemmas for plain and absorbing

!903 · created Apr 01, 2023 by William Mansky
- 19
updated Oct 13, 2023
Draft: parameterize the algebra folder by the stepindex type for integration with Transfinite Iris

!888 · created Feb 05, 2023 by Lennard Gäher
- 1
- 74
updated Dec 02, 2023
WIP: Step Update modality demonstration

!887 · created Jan 30, 2023 by Jonas Kastberg
- 1
- 0
updated May 26, 2023
get rid of Z.to_nat coercion, and add some Z-based APIs: big_sepL, and HeapLang arrays

!883 · created Jan 12, 2023 by Ralf Jung
updated Jan 12, 2023