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