diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index cf4142b6ca..863739a4eb 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -723,6 +723,14 @@ fun stx expectedType? => do
   let newStx   := args.foldSepRevArgs (fun arg r => mkAppStx consId #[arg, r]) nilId;
   elabTerm newStx expectedType?
 
+@[builtinTermElab «arrayLit»] def elabArrayLit : TermElab :=
+fun stx expectedType? => do
+  match_syntax stx.val with
+  | `(#[$args*]) => do
+    newStx ← `(List.toArray [$args*]);
+    withMacroExpansion stx.val (elabTerm newStx expectedType?)
+  | _ => throwError stx.val "unexpected array literal syntax"
+
 def elabExplicitUniv (stx : Syntax) : TermElabM (List Level) :=
 pure [] -- TODO
 
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index 293d66a456..cc5bb131b9 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -150,3 +150,4 @@ f a
 
 #eval run "#check fun x => foo x x.w s4"
 #eval run "#check bla (fun x => x.w) s4"
+#eval run "#check #[1, 2, 3]"