From 6f5bb3e8963bc85e8b3f0a1cd62d53a0ec4c498b Mon Sep 17 00:00:00 2001
From: Kitamado <47292598+Seasawher@users.noreply.github.com>
Date: Mon, 17 Feb 2025 04:26:23 +0900
Subject: [PATCH] fix: allow trailing comma in array syntax (#7055)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR improves array and vector literal syntax by allowing trailing
commas. For example, `#[1, 2, 3,]`.

see: [Why Are Trailing Commas Not Allowed in Array
Literals?](https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Why.20Are.20Trailing.20Commas.20Not.20Allowed.20in.20Array.20Literals.3F)

Note: we need to preserve the current name for the array syntax
(`«term#[_,]»`) to avoid a bootstrapping issue. The `FromJson`/`ToJson`
deriving handlers use array syntax in macros, and the stage0 version is
used in most of the prelude.
---
 src/Init/Data/Array/Basic.lean  | 2 +-
 src/Init/Data/Vector/Basic.lean | 2 +-
 tests/lean/run/array1.lean      | 2 ++
 3 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index c0c37b8299..10b473c64f 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -19,7 +19,7 @@ universe u v w
 /-! ### Array literal syntax -/
 
 /-- Syntax for `Array α`. -/
-syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
+syntax (name := «term#[_,]») "#[" withoutPosition(term,*,?) "]" : term
 
 macro_rules
   | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
diff --git a/src/Init/Data/Vector/Basic.lean b/src/Init/Data/Vector/Basic.lean
index 8da7af928e..1659dc58d9 100644
--- a/src/Init/Data/Vector/Basic.lean
+++ b/src/Init/Data/Vector/Basic.lean
@@ -31,7 +31,7 @@ abbrev Array.toVector (xs : Array α) : Vector α xs.size := .mk xs rfl
 namespace Vector
 
 /-- Syntax for `Vector α n` -/
-syntax "#v[" withoutPosition(sepBy(term, ", ")) "]" : term
+syntax (name := «term#v[_,]») "#v[" withoutPosition(term,*,?) "]" : term
 
 open Lean in
 macro_rules
diff --git a/tests/lean/run/array1.lean b/tests/lean/run/array1.lean
index 9aa350cb9c..e08478f634 100644
--- a/tests/lean/run/array1.lean
+++ b/tests/lean/run/array1.lean
@@ -2,6 +2,8 @@
 
 def v : Array Nat := Array.mk [1, 2, 3, 4]
 
+#guard v == #[1, 2, 3, 4, ]
+
 def w : Array Nat :=
 (mkArray 9 1).push 3