fix: allow trailing comma in array syntax (#7055)

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

@@ -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,* ])

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

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