tests/heap_lang.v · a361b1732c4cd7a173b9a1eccb32713abb839b0a · Iris / Iris · GitLab

Find file Blame History Permalink

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