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

doc: Syntax.topDown

Browse source
This commit is contained in:
Sebastian Ullrich 2021-03-11 18:42:36 +01:00 • committed by Leonardo de Moura
parent ddff87f7f5
commit cb5050bb7f
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Syntax.lean
View file

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