Merge branch 'robbert/wp_apply_pure' into 'master'
Make `wp_apply` perform `wp_pure` in small steps until the lemma matches the goal. See merge request iris/iris!587
No related branches found
No related tags found
Showing
- CHANGELOG.md 3 additions, 0 deletionsCHANGELOG.md
- iris_heap_lang/lib/array.v 6 additions, 6 deletionsiris_heap_lang/lib/array.v
- iris_heap_lang/lib/assert.v 2 additions, 2 deletionsiris_heap_lang/lib/assert.v
- iris_heap_lang/lib/increment.v 4 additions, 4 deletionsiris_heap_lang/lib/increment.v
- iris_heap_lang/lib/spawn.v 2 additions, 2 deletionsiris_heap_lang/lib/spawn.v
- iris_heap_lang/proofmode.v 38 additions, 25 deletionsiris_heap_lang/proofmode.v
- tests/heap_lang.v 3 additions, 3 deletionstests/heap_lang.v
- tests/heap_lang_proph.v 1 addition, 1 deletiontests/heap_lang_proph.v
- tests/one_shot.v 5 additions, 5 deletionstests/one_shot.v
- tests/one_shot_once.v 4 additions, 4 deletionstests/one_shot_once.v
- tests/tree_sum.v 1 addition, 1 deletiontests/tree_sum.v
Loading
Please register or sign in to comment