diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 2b851188f1..fc09a93c28 100644
--- a/src/Lean/Syntax.lean
+++ b/src/Lean/Syntax.lean
@@ -180,6 +180,10 @@ structure TopDown where
   firstChoiceOnly : Bool
   stx : Syntax
 
+/--
+`for _ in stx.topDown` iterates through each node and leaf in `stx` top-down, left-to-right.
+If `firstChoiceOnly` is `true`, only visit the first argument of each choice node.
+-/
 def topDown (stx : Syntax) (firstChoiceOnly := false) : TopDown := ⟨firstChoiceOnly, stx⟩
 
 partial instance : ForIn m TopDown Syntax where