iris_heap_lang/lib/spawn.v · d7b84ad421295a9f53212f49e44cdb36a272b8e8 · William Mansky / Iris · GitLab

Snippets Groups Projects

Forked from Iris / Iris

1682 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.
```

spawn.v 2.87 KiB