Merge Requests · Iris

add iSplitWith tactic for convenient conjunction monotonicity

iris!141 · opened Apr 23, 2018 by Ralf Jung gen_proofmode T-proofmode
- CLOSED
- 1
updated Jul 13, 2018
fix applying big_sepL_singleton

iris!168 · opened Jul 04, 2018 by Ralf Jung gen_proofmode
- CLOSED
- 2
updated Jul 04, 2018
WIP: fix for stronger CAS requirements

examples!10 · opened Jul 01, 2018 by Ralf Jung ci/gen_proofmode
- CLOSED
- 1
updated Jul 04, 2018
Reserve more notation in `integers.v`.

stdpp!22 · opened Nov 29, 2017 by David Swasey
- CLOSED
- 3
updated Jun 20, 2018
Adding telescopes and some useful lemmas.

iris!61 · opened Aug 28, 2017 by Joshua Yanovski
- CLOSED
- 19
updated Jun 15, 2018
WIP: Support sequential languages.

iris!38 · opened Dec 17, 2016 by David Swasey
- CLOSED
- 16
updated Jun 14, 2018
Implement `big_sepL_delete`

iris!136 · opened Mar 27, 2018 by Dan Frumin
- CLOSED
- 1
updated Mar 27, 2018
Factor plainly out of main BI interface

iris!98 · opened Dec 06, 2017 by Ralf Jung Generalized Proofmode Merger gen_proofmode T-proofmode
- CLOSED
- 171
updated Mar 03, 2018
add exact_vm_cast

stdpp!28 · opened Mar 01, 2018 by Ralf Jung
- CLOSED
- 5
updated Mar 01, 2018
Syntax `iAssert (Q with spat) as ...`

iris!117 · opened Feb 19, 2018 by Robbert Krebbers gen_proofmode
- CLOSED
- 8
updated Feb 21, 2018
Saved predicates

iris!72 · opened Oct 25, 2017 by Amin Timany Iris 3.1
- CLOSED
- 16
updated Nov 03, 2017
Add filter for gmap

stdpp!6 · opened Sep 28, 2017 by Hai Dang
- CLOSED
- 13
updated Oct 27, 2017
Resolve "Disjoint uses ⊥ (U+22A5 -- UP TACK) but should use ⟂ (U+27C2 -- PERPENDICULAR)"

stdpp!11 · opened Oct 27, 2017 by Jacques-Henri Jourdan
- CLOSED
- 0
updated Oct 27, 2017
WIP: unfold typeclass opaque definitions in proof mode

iris!39 · opened Jan 03, 2017 by Ralf Jung
- CLOSED
- 7
updated Oct 10, 2017
Adding location equality.

lambda-rust!7 · opened Aug 29, 2017 by Joshua Yanovski
- CLOSED
- 19
updated Sep 28, 2017
Jh/done contradiction

iris!48 · opened Feb 13, 2017 by Jacques-Henri Jourdan
- CLOSED
- 10
updated Feb 13, 2017
Make the setoid equivalence and metric for excl and csum independent from the chosen OFE

iris!44 · opened Jan 28, 2017 by Jacques-Henri Jourdan
- CLOSED
- 80
updated Feb 09, 2017
WIP: load an options file everywhere to avoid repetition

iris!45 · opened Feb 03, 2017 by Ralf Jung
- CLOSED
- 14
updated Feb 07, 2017
Cancellable elements.

iris!43 · opened Jan 27, 2017 by Jacques-Henri Jourdan
- CLOSED
- 31
updated Feb 01, 2017
WIP: Make `make quick` make quickly.

iris!36 · opened Dec 14, 2016 by Janno Iris 3.0
- CLOSED
- 23
updated Jan 03, 2017