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

doc: documentation of p,+ macro should mention that it maps to sepBy1, not sepBy (#9876)

Browse source 
This PR fixes doc issue of p,+ macro,which maps to sepBy1(p, ",") while
doc says that it maps to sepBy(p, ",").

Closes https://github.com/leanprover/lean4/issues/9873
This commit is contained in:
nnarek 2025-08-19 15:54:47 +04:00 • committed by GitHub
parent cd729660ed
commit b75fbe7a40
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/Notation.lean
View file

@ -226,7 +226,7 @@ results. It has arity 1, and auto-groups its component parser if needed.
-/
macro:arg x:stx:max ",*" : stx => `(stx| sepBy($x, ",", ", "))
/--
`p,+` is shorthand for `sepBy(p, ",")`. It parses 1 or more occurrences of
`p,+` is shorthand for `sepBy1(p, ",")`. It parses 1 or more occurrences of
`p` separated by `,`, that is: `p | p,p | p,p,p | ...`.
It produces a `nullNode` containing a `SepArray` with the interleaved parser