From c43450f027a0b26727dec29651392f37051fd7eb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 19 Sep 2020 14:59:00 -0700
Subject: [PATCH] feat: macros for the syntax category

This is the last of a series of commits for adding this feature.
---
 src/Lean/Elab/Quotation.lean |  1 +
 tests/lean/run/stxMacro.lean | 18 ++++++++++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 tests/lean/run/stxMacro.lean

diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 2be476a55e..7a19240085 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/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 -/
 
diff --git a/tests/lean/run/stxMacro.lean b/tests/lean/run/stxMacro.lean
new file mode 100644
index 0000000000..0474ce332b
--- /dev/null
+++ b/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