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

doc: update docstring of Lean.Parser.Tactic.Grind.first (#12998)

Browse source 
This PR updates the docstring for `Lean.Parser.Tactic.Grind.first`,
which changed syntax in #10828.
This commit is contained in:
Chris Henson 2026-03-22 12:54:33 -04:00 • committed by GitHub
parent 8f6411ad57
commit c9708e7bd7
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Grind/Interactive.lean
View file

@ -205,7 +205,7 @@ macro:1 x:grind tk:" <;> " y:grind:2 : grind => `(grind|
with_annotate_state $tk skip
all_goals $y:grind)
/-- `first | tac | ...` runs each `tac` until one succeeds, or else fails. -/
/-- `first (tac) ...` runs each `tac` until one succeeds, or else fails. -/
syntax (name := first) "first " withPosition((ppDedent(ppLine) colGe "(" grindSeq ")")+) : grind
/-- `try tac` runs `tac` and succeeds even if `tac` failed. -/