From 1db4c77d4e5ccb3cb9718ee4d073ed52532af330 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 Jul 2022 07:27:54 -0400
Subject: [PATCH] document wp_smart_apply

---
 docs/heap_lang.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/docs/heap_lang.md b/docs/heap_lang.md
index aeaa29915..705480cd1 100644
--- a/docs/heap_lang.md
+++ b/docs/heap_lang.md
@@ -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`.
 
-- 
GitLab