From e04d67f55fbc7ab104016549e818b03fd73a63a1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Wed, 31 May 2023 05:32:55 -0700
Subject: [PATCH] chore: expand docstring for `TransformStep.visit`

---
 src/Lean/Meta/Transform.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Transform.lean b/src/Lean/Meta/Transform.lean
index 034cd574ed..bcba08287a 100644
--- a/src/Lean/Meta/Transform.lean
+++ b/src/Lean/Meta/Transform.lean
@@ -10,7 +10,10 @@ namespace Lean
 inductive TransformStep where
   /-- Return expression without visiting any subexpressions. -/
   | done (e : Expr)
-  /-- Visit expression (which should be different from current expression) instead. -/
+  /--
+  Visit expression (which should be different from current expression) instead.
+  The new expression `e` is passed to `pre` again.
+  -/
   | visit (e : Expr)
   /--
   Continue transformation with the given expression (defaults to current expression).