- 10 Jul, 2020 2 commits
-
-
Ralf Jung authoredLICENSE-CODE: Clarify which BSD license is being used See merge request iris/iris!472
-
-
- 04 Jul, 2020 1 commit
-
-
Ralf Jung authored
-
- 03 Jul, 2020 1 commit
-
-
Ralf Jung authored
-
- 02 Jul, 2020 4 commits
-
-
Ralf Jung authored
Mention change to lemmas in changelog See merge request iris/iris!469
-
Simon Friis Vindum authored -
Ralf Jung authored
adjust notation for step-taking updates See merge request iris/iris!462
-
Ralf Jung authored
-
- 01 Jul, 2020 2 commits
-
-
Robbert Krebbers authored
Add lemmas for creating big op from duplicable resource See merge request iris/iris!468
-
Robbert Krebbers authored
-
- 30 Jun, 2020 1 commit
-
-
Simon Friis Vindum authored
-
- 29 Jun, 2020 4 commits
-
-
Simon Friis Vindum authored
-
Robbert Krebbers authored
-
Ralf Jung authored
-
Simon Friis Vindum authored
-
- 26 Jun, 2020 3 commits
- 19 Jun, 2020 4 commits
-
-
Ralf Jung authored
-
Ralf Jung authored
-
Ralf Jung authored
Port to Coq #12512. See merge request iris/iris!465
-
Robbert Krebbers authored
-
- 18 Jun, 2020 6 commits
-
-
Ralf Jung authored
-
-
Ralf Jung authored
-
Robbert Krebbers authored
Add natural numbers with min RA Closes #324 See merge request iris/iris!461
-
Simon Friis Vindum authored
-
Ralf Jung authored
-
- 17 Jun, 2020 3 commits
-
-
Ralf Jung authored
-
Simon Friis Vindum authored
-
Simon Friis Vindum authored
Add IdempP instances for min_nat and max_nat. Move additional numbers related lemmas and instances into the numbers file.
-
- 16 Jun, 2020 1 commit
-
-
Simon Friis Vindum authored
-
- 15 Jun, 2020 2 commits
-
-
Robbert Krebbers authored
Use [fill K] in tac_wp_pure See merge request iris/iris!463
-
Tej Chajed authored
This is more consistent with other tac_wp tactics for HeapLang and also a tiny bit more efficient, which is good to embody in the basic tactics so derived code follows the same patterns.
-
- 13 Jun, 2020 1 commit
-
-
Simon Friis Vindum authored
-
- 12 Jun, 2020 2 commits
-
-
Robbert Krebbers authored
Fix error message when with [% //] fails Closes #325 See merge request iris/iris!460
-
Tej Chajed authored
Fixes #325. Also added a tests for the various `iSpecialize` error cases involving the `[%]` and `[//]` specialization patterns.
-
- 11 Jun, 2020 3 commits
-
-
Ralf Jung authored
Factor out lemma `löb_weak`. See merge request iris/iris!459
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
