Merge Requests · Iris · GitLab

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
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
rename valid -> emp_valid

iris!131 · opened Mar 19, 2018 by Ralf Jung Generalized Proofmode Merger gen_proofmode
- MERGED
- 15
updated Jul 13, 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
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
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
Use solely canonical structures for language hierarchy.

iris!90 · opened Nov 23, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 12
updated Nov 24, 2017
Get rid of `ofe_fun`, it was just a non-dependently typed version of `iprod`

iris!88 · opened Nov 21, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 34
updated Nov 28, 2017
do not make use of wp_bind_inv unnecessarily

iris!87 · opened Nov 21, 2017 by Ralf Jung Iris 3.1
- MERGED
- 16
updated Nov 24, 2017
saved predicates: use ofe_fun, not ofe_mor

iris!86 · opened Nov 21, 2017 by Ralf Jung Iris 3.1
- MERGED
- 9
updated Nov 22, 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
Get rid of `later_proper'`

iris!82 · opened Nov 11, 2017 by Robbert Krebbers Iris 3.1
- MERGED
- 1
updated Nov 11, 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
Add stuckness bits to WP.

iris!80 · opened Nov 09, 2017 by David Swasey Iris 3.1
- MERGED
- 79
updated Feb 02, 2018
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
generalize savedProp to let the user control the position of the type-level later

iris!76 · opened Oct 29, 2017 by Ralf Jung Iris 3.1
- MERGED
- 45
updated Nov 18, 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
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
Notation for disjointness: replace ⊥ with ##, so that ⊥ can be used for bottom.

iris!73 · opened Oct 27, 2017 by Jacques-Henri Jourdan Iris 3.1
- MERGED
- 1
updated Oct 29, 2017

Prev
1
2
3
4
5
6
7
…
46
Next