chore: remove list/array literal builtin parsers

src/Lean/Elab/Term.lean

@@ -1129,20 +1129,6 @@ private def mkTacticMVar (type : Expr) (tacticCode : Syntax) : TermElabM Expr :=
   | some expectedType => mkTacticMVar expectedType stx
   | none => throwError ("invalid 'by' tactic, expected type has not been provided")
 
-@[builtinMacro Lean.Parser.Term.listLit] def expandListLit : Macro := fun stx =>
-  let openBkt  := stx[0]
-  let args     := stx[1]
-  let closeBkt := stx[2]
-  let consId   := mkIdentFrom openBkt `List.cons
-  let nilId    := mkIdentFrom closeBkt `List.nil
-  return args.getSepArgs.foldr (init := nilId) fun arg r =>
-    Syntax.mkApp consId #[arg, r]
-
-@[builtinMacro Lean.Parser.Term.arrayLit] def expandArrayLit : Macro := fun stx =>
-  match_syntax stx with
-  | `(#[$args*]) => `(List.toArray [$args*])
-  | _            => throw $ Macro.Exception.error stx "unexpected array literal syntax"
-
 def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
   let lctx ← getLCtx
   let view := extractMacroScopes n

src/Lean/Parser/Term.lean

@@ -88,8 +88,6 @@ def structInstField  := ppGroup $ parser! structInstLVal >> " := " >> termParser
 def typeSpec := parser! " : " >> termParser
 def optType : Parser := optional typeSpec
 @[builtinTermParser] def subtype := parser! "{ " >> ident >> optType >> " // " >> termParser >> " }"
-@[builtinTermParser] def listLit := parser! "[" >> sepBy termParser ", " true >> "]"
-@[builtinTermParser] def arrayLit := parser! "#[" >> sepBy termParser ", " true >> "]"
 @[builtinTermParser] def explicit := parser! "@" >> termParser maxPrec
 @[builtinTermParser] def inaccessible := parser! ".(" >> termParser >> ")"
 def binderIdent : Parser  := ident <|> hole