- 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 4 commits
-
-
Ralf Jung authored
Factor out lemma `löb_weak`. See merge request iris/iris!459
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- 08 Jun, 2020 1 commit
-
-
Ralf Jung authored
-
- 07 Jun, 2020 2 commits
- 06 Jun, 2020 2 commits
- 04 Jun, 2020 1 commit
-
-
Ralf Jung authored
-
- 03 Jun, 2020 1 commit
-
-
Ralf Jung authored
-
- 01 Jun, 2020 1 commit
-
-
Ralf Jung authored
-
- 30 May, 2020 1 commit
-
-
Ralf Jung authored
-
- 29 May, 2020 6 commits
- 28 May, 2020 2 commits
-
-
Robbert Krebbers authored
Fix `forall` parsing. See merge request !432
-
Gregory Malecha authored
-
