Merge Requests · Iris

A simple type class based canceler for natural numbers.

stdpp!26 · opened Feb 07, 2018 by Robbert Krebbers
- MERGED
- 5
updated Feb 08, 2018
Generic `iAlways` tactic. 3 of 3 tasks completed

iris!111 · opened Feb 06, 2018 by Robbert Krebbers gen_proofmode
- MERGED
- 23
updated Feb 08, 2018
Various improvements to iFrame

iris!110 · opened Feb 02, 2018 by Robbert Krebbers
- MERGED
- 19
updated Feb 08, 2018
Stronger `iNext` that performs arithmetic cancelation 3 of 3 tasks completed

iris!109 · opened Jan 30, 2018 by Robbert Krebbers
- MERGED
- 26
updated Mar 22, 2018
Consistently name `wp_value_inv`

iris!108 · opened Jan 19, 2018 by Robbert Krebbers
- MERGED
- 5
updated Jan 24, 2018
Special proof mode class for adding a modality to a goal

iris!107 · opened Jan 16, 2018 by Robbert Krebbers
- MERGED
- 2
updated Feb 12, 2018
Type classes for updates properties

iris!106 · opened Jan 15, 2018 by Jacques-Henri Jourdan gen_proofmode
- MERGED
- 18
updated Jan 18, 2018
Add a Notation for `sn`: strongly normalizing.

stdpp!25 · opened Jan 12, 2018 by Robbert Krebbers
- MERGED
- 1
updated Jan 13, 2018
`iEval ... in ...` for performing a tactic in an invidual proofmode hypothesis

iris!105 · opened Dec 31, 2017 by Robbert Krebbers
- MERGED
- 14
updated Jan 24, 2018
Consistent handling of pure implication and forall

iris!104 · opened Dec 20, 2017 by Robbert Krebbers T-proofmode
- MERGED
- 6
updated Dec 21, 2017
BI -> Bi, to match our convention

iris!103 · opened Dec 20, 2017 by Ralf Jung gen_proofmode
- MERGED
- 2
updated Jul 13, 2018
Add the spanning tree algorithm.

examples!3 · opened Dec 14, 2017 by Amin Timany
- MERGED
- 4
updated Jan 25, 2019
Amin/logrel

examples!2 · opened Dec 14, 2017 by Amin Timany
- MERGED
- 5
updated Jan 25, 2019
Type classes for fancy updates and basic updates.

iris!101 · opened Dec 11, 2017 by Jacques-Henri Jourdan gen_proofmode
- MERGED
- 12
updated Dec 14, 2017
Proof mode support for monotonous predicates.

iris!100 · opened Dec 11, 2017 by Jacques-Henri Jourdan janno/monfun T-proofmode
- MERGED
- 53
updated Jul 13, 2018
Prove that uPred is complete even if we remove the validity restriction in uPred_closed.

iris!99 · opened Dec 06, 2017 by Jacques-Henri Jourdan Iris 3.1
- MERGED
- 21
updated Dec 08, 2017
typeclass comments

stdpp!24 · opened Dec 05, 2017 by Ralf Jung
- MERGED
- 0
updated Dec 05, 2017
Add all the usual binary operators to heap_lang.

iris!97 · opened Dec 05, 2017 by Robbert Krebbers
- MERGED
- 17
updated Mar 19, 2018
Add atomic fetch-and-add operation to heap_lang

iris!96 · opened Dec 04, 2017 by Robbert Krebbers
- MERGED
- 2
updated Dec 05, 2017
Remove plainly_exist_1 from the BI axioms.

iris!95 · opened Dec 04, 2017 by Jacques-Henri Jourdan gen_proofmode T-proofmode
- MERGED
- 21
updated Jul 13, 2018