From b75fbe7a405ea41a87cf0095a10f36fa8b35efbb Mon Sep 17 00:00:00 2001
From: nnarek <49597137+nnarek@users.noreply.github.com>
Date: Tue, 19 Aug 2025 15:54:47 +0400
Subject: [PATCH] doc: documentation of p,+ macro should mention that it maps
 to sepBy1, not sepBy (#9876)

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
---
 src/Init/Notation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 21a74c7581..e582d03286 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -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