From cb5050bb7fdb1afb7c8affaa7e2a51640ca074d9 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 11 Mar 2021 18:42:36 +0100
Subject: [PATCH] doc: Syntax.topDown

---
 src/Lean/Syntax.lean | 4 ++++
 1 file changed, 4 insertions(+)

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