Merge Requests · Iris

Factor out solve_proper_prepare

stdpp!19 · opened Nov 16, 2017 by Ralf Jung
- MERGED
- 4
updated Nov 18, 2017
Improved treatment of anonymous hypotheses in the proof mode

iris!83 · opened Nov 11, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 6
updated Nov 16, 2017
Fix typo in definition of weakest pre in documentation.

iris!84 · opened Nov 14, 2017 by Joseph Tassarotti
- MERGED
- 1
updated Nov 15, 2017
Provide an Infinite typeclass and a generic implementation of Fresh.

stdpp!13 · opened Oct 31, 2017 by Ghost User
- MERGED
- 16
updated Nov 12, 2017
Make `fmap` left associative.

stdpp!16 · opened Nov 08, 2017 by Robbert Krebbers
- MERGED
- 1
updated Nov 12, 2017
add later_ne; make later_proper match the other _proper lemmas

iris!81 · opened Nov 11, 2017 by Ralf Jung Iris 3.1
- MERGED
- 8
updated Nov 11, 2017
Get rid of `later_proper'`

iris!82 · opened Nov 11, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 1
updated Nov 11, 2017
Use `stdpp_scope` for all notations.

stdpp!17 · opened Nov 09, 2017 by Robbert Krebbers
- MERGED
- 10
updated Nov 11, 2017
Add progress bit to WP.

iris!37 · opened Dec 17, 2016 by David Swasey Iris 3.1
- MERGED
- 68
updated Nov 09, 2017
rename sub_values -> sub_redexes_are_values

iris!79 · opened Nov 04, 2017 by Ralf Jung Iris 3.1
- MERGED
- 7
updated Nov 07, 2017
add a strong form of atomicity, for weak forms of weakest-pre

iris!77 · opened Oct 29, 2017 by Ralf Jung Iris 3.1
- MERGED
- 22
updated Nov 05, 2017
Common tactic machinery for symbolic execution of pure reductions

iris!64 · opened Sep 20, 2017 by Dan Frumin
- MERGED
- 40
updated Nov 05, 2017
Make proofnode notation more robust in the context of import order

iris!75 · opened Oct 29, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 13
updated Nov 05, 2017
Make atomic a type class.

iris!78 · opened Nov 04, 2017 by Robbert Krebbers
- MERGED
- 4
updated Nov 04, 2017
Minor documentation fixes

stdpp!14 · opened Oct 31, 2017 by Ghost User
- MERGED
- 1
updated Oct 31, 2017
Put the entire development under the BSD license

lambda-rust!9 · opened Oct 30, 2017 by Ralf Jung
- MERGED
- 7
updated Oct 30, 2017
Add poison

lambda-rust!8 · opened Oct 30, 2017 by Ralf Jung
- MERGED
- 4
updated Oct 30, 2017
Notation for disjointness: replace ⊥ with ##, so that ⊥ can be used for bottom.

stdpp!12 · opened Oct 27, 2017 by Jacques-Henri Jourdan
- MERGED
- 11
updated Oct 29, 2017
Rules for fancy updates and plain propositions.

iris!74 · opened Oct 27, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 5
updated Oct 29, 2017
The plainness modality

iris!71 · opened Oct 18, 2017 by Amin Timany Iris 3.1
- MERGED
- 91
updated Oct 29, 2017