Skip to content
Snippets Groups Projects
Commit 1db4c77d authored by Ralf Jung's avatar Ralf Jung
Browse files

document wp_smart_apply

parent a32f36a9
No related branches found
No related tags found
No related merge requests found
......@@ -104,6 +104,8 @@ Further tactics:
- `wp_apply pm_trm`: Apply a lemma whose conclusion is a `WP`, automatically
applying `wp_bind` as needed. See the [ProofMode docs](./proof_mode.md) for an
explanation of `pm_trm`.
- `wp_smart_apply pm_trm`: like `wp_apply`, but also performs pure reduction
steps (same as `wp_pure`) to reveal a redex that matches `pm_trm`.
There is no tactic for `Fork`, just do `wp_apply wp_fork`.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment