max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: expand docstring for TransformStep.visit

Browse source
This commit is contained in:
Leonardo de Moura 2023-05-31 05:32:55 -07:00
parent efe75b2b16
commit e04d67f55f
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Meta/Transform.lean
View file

@ -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).