iris_heap_lang/lib/increment.v · a361b1732c4cd7a173b9a1eccb32713abb839b0a · Yixuan Chen / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

6937 commits behind the upstream repository.

4 years ago
a361b173
Change `wp_apply` so it no longer performs `wp_pures`, and add new tactic `wp_smart_apply` · a361b173
Robbert Krebbers authored 4 years ago
```
that performs `wp_pure` in small steps until the lemma matches the goal.
```
a361b173

History
Change `wp_apply` so it no longer performs `wp_pures`, and add new tactic `wp_smart_apply`
Robbert Krebbers authored 4 years ago
```
that performs `wp_pure` in small steps until the lemma matches the goal.
```