From f752ce2db94892fe70686730fb594bc6e7da5159 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Tue, 22 Oct 2024 02:33:46 +0100
Subject: [PATCH] doc: stub for ellipsis notation (#5794)

This is certainly better than no documentation, though it's not obvious
to me whether the `_` insertion is greedy, lazy, or somewhere in
between.
---
 src/Lean/Parser/Term.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 1e450cdf8b..15d4cc1a0d 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -819,6 +819,7 @@ We use them to implement `macro_rules` and `elab_rules`
 
 def namedArgument  := leading_parser (withAnonymousAntiquot := false)
   atomic ("(" >> ident >> " := ") >> withoutPosition termParser >> ")"
+/-- In a function application, `..` notation inserts zero or more `_` placeholders. -/
 def ellipsis       := leading_parser (withAnonymousAntiquot := false)
   ".." >> notFollowedBy (checkNoWsBefore >> ".") "`.` immediately after `..`"
 def argument       :=