Merge Requests · Iris · GitLab

Enable test suite to check printed output

iris!147 · opened May 17, 2018 by Ralf Jung gen_proofmode
- MERGED
- 4
updated May 20, 2018
fix `head_stuck`

iris!144 · opened May 03, 2018 by Glen Mével
- MERGED
- 5
updated May 11, 2018
Derive löb induction from later introduction and guarded fixpoints

iris!145 · opened May 03, 2018 by Ralf Jung gen_proofmode
- MERGED
- 1
- 13
updated May 08, 2018
Fix a file broken due to wp_binop changes

examples!7 · opened Apr 30, 2018 by Dan Frumin
- MERGED
- 1
updated Apr 30, 2018
Get rid of tvProp by using thread identifiers and ghost state.

gpfsl!2 · opened Apr 26, 2018 by Jacques-Henri Jourdan
- MERGED
- 12
updated Apr 27, 2018
proofmode: make it possible for class_instances to use the proofmode

iris!142 · opened Apr 23, 2018 by Ralf Jung gen_proofmode
- MERGED
- 3
updated Apr 25, 2018
Add more examples from the lecture notes.

examples!6 · opened Apr 23, 2018 by Aleš Bizjak
- MERGED
- 1
updated Apr 24, 2018
Let `done` and friends fail when the proofmode goal is an evar.

iris!140 · opened Apr 20, 2018 by Robbert Krebbers gen_proofmode
- MERGED
- 4
updated Apr 22, 2018
gmultiset RA

iris!138 · opened Apr 10, 2018 by Dan Frumin
- MERGED
- 10
updated Apr 11, 2018
Weaken axioms for BI embeddings

iris!137 · opened Apr 04, 2018 by Robbert Krebbers gen_proofmode
- MERGED
- 27
updated Apr 09, 2018
Notations for relations with explicit type arguments

stdpp!30 · opened Apr 05, 2018 by Robbert Krebbers
- MERGED
- 3
updated Apr 06, 2018
add notation to define the PROP we use for a particular turnstile

iris!134 · opened Mar 21, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 44
updated Apr 05, 2018
Extend ElimModal with Boolean flags to specify whether it operates on the…

iris!129 · opened Mar 15, 2018 by Robbert Krebbers Generalized Proofmode Merger gen_proofmode
- MERGED
- 11
updated Apr 05, 2018
more consistent lemma naming

iris!135 · opened Mar 22, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 1
updated Apr 03, 2018
rename affinely_persistently -> intuitionistically; and make it a TC-opaque definition

iris!130 · opened Mar 19, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode T-proofmode
- MERGED
- 28
updated Mar 22, 2018
move Frame instances to their own file

iris!133 · opened Mar 21, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 4
updated Mar 22, 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
Add all the usual binary operators to heap_lang.

iris!97 · opened Dec 05, 2017 by Robbert Krebbers
- MERGED
- 17
updated Mar 19, 2018
Store a counter in `Envs` to assign fresh names with `iFresh`.

iris!128 · opened Mar 12, 2018 by Joseph Tassarotti gen_proofmode
- MERGED
- 10
updated Mar 15, 2018
Renaming and notations for modalities gen_proofmode

iris!126 · opened Mar 04, 2018 by Robbert Krebbers gen_proofmode
- MERGED
- 5
updated Mar 04, 2018

Prev
1
…
35
36
37
38
39
40
41
42
43
…
46
Next