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