feat: macros for the syntax category

This is the last of a series of commits for adding this feature.

src/Lean/Elab/Quotation.lean

@@ -134,6 +134,7 @@ stx ← quoteSyntax (elimAntiquotChoices quoted);
 @[builtinTermElab Parser.Term.quot] def elabTermQuot : TermElab := adaptExpander stxQuot.expand
 @[builtinTermElab Parser.Term.funBinder.quot] def elabfunBinderQuot : TermElab := adaptExpander stxQuot.expand
 @[builtinTermElab Parser.Tactic.quot] def elabTacticQuot : TermElab := adaptExpander stxQuot.expand
+@[builtinTermElab Parser.Term.stx.quot] def elabStxQuot : TermElab := adaptExpander stxQuot.expand
 
 /- match_syntax -/
 

tests/lean/run/stxMacro.lean

@@ -0,0 +1,18 @@
+new_frontend
+
+-- Macro for the `syntax` category
+macro "many " x:stx : stx => `(stx| ($x)*)
+
+syntax "sum! " (many term:max) : term
+
+macro_rules
+| `(sum! $x*) => do
+  r ← `(0);
+  x.foldlM (fun r elem => `($r + $elem)) r
+
+#check sum! 1 2 3
+#eval sum! 1 2 3
+#check sum!
+
+theorem ex : sum! 1 2 3 = 6 :=
+rfl