Issues · Iris / Iris

New issue

Stripping laterN from pure propositions when proving laterN *without except-0*

#237 · opened Apr 15, 2019 by Paolo G. Giarrusso
- 1
updated Apr 15, 2019
Non-expansiveness for big ops

#236 · opened Apr 07, 2019 by Dan Frumin
- 0
updated Apr 07, 2019
Documentation for the algebra folder

#235 · opened Mar 30, 2019 by Robbert
- 1
- 1
updated Mar 30, 2019
Syntactic type system for heap_lang 0 of 2 tasks completed

#234 · opened Mar 29, 2019 by Robbert Heap lang
- 18
updated Apr 08, 2019
Investigate slowdown caused by gset change

#232 · opened Mar 14, 2019 by Ralf Jung
- 1
- 9
updated Apr 23, 2019
Allow swapping later^i and forall, later, etc.

#231 · opened Mar 02, 2019 by Paolo G. Giarrusso
- 3
updated Mar 03, 2019
Introduction of predicate over expression in WP

#228 · opened Feb 19, 2019 by Jonas Kastberg
- 19
updated Feb 28, 2019
Provide a convenient way to define non-recursive ghost state

#227 · opened Feb 19, 2019 by Ralf Jung
- 1
- 2
updated Feb 20, 2019
Get rid of the core, define persistence otherwise

#224 · opened Dec 18, 2018 by Ralf Jung
- 8
updated Dec 21, 2018
Coqdocs should link to std++ coqdocs

#221 · opened Nov 30, 2018 by Ralf Jung
- 1
updated Nov 30, 2018
Replace most occurences of `.. || ..` by `first [..|..]`

#216 · opened Oct 14, 2018 by Robbert
- 2
updated Oct 15, 2018
Explore getting rid of implication

#215 · opened Oct 13, 2018 by Ralf Jung
- 7
updated Oct 15, 2018
Moving stuff out of the intuitionistic context

#213 · opened Oct 04, 2018 by Robbert Proofmode
- 0
updated Oct 04, 2018
iMod: Control which modality is reduced

#212 · opened Oct 03, 2018 by Ralf Jung Proofmode
- 10
updated Oct 05, 2018
Masks are coPsets in the Coq development, not arbitrary subsets of natural numbers

#211 · opened Oct 01, 2018 by Joseph Tassarotti
- 1
updated Oct 01, 2018
Generic subset construction for RAs

#210 · opened Aug 29, 2018 by Ralf Jung
- 2
updated Sep 18, 2018
Make notation for pure and plainly affine

#205 · opened Jul 13, 2018 by Ralf Jung
- 1
updated Jul 31, 2018
Seal off local and frame-preserving update

#203 · opened Jul 05, 2018 by Ralf Jung
- 0
updated Jul 05, 2018
Use of `Into`/`From`/`As`/`Is` prefixes of classes is inconsistent

#202 · opened Jun 18, 2018 by Robbert
- 0
updated Jun 18, 2018
Extend `iApply` to deal with pure goals

#196 · opened Jun 07, 2018 by Glen Mével
- 1
- 1
updated Apr 03, 2019