From 73fce217f645cfb9649f676a4a96103d35b5a74a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 18 Jul 2022 23:50:41 -0400
Subject: [PATCH] test: for issue #1321

---
 tests/lean/1321.lean              | 11 +++++++++++
 tests/lean/1321.lean.expected.out |  4 ++++
 2 files changed, 15 insertions(+)
 create mode 100644 tests/lean/1321.lean
 create mode 100644 tests/lean/1321.lean.expected.out

diff --git a/tests/lean/1321.lean b/tests/lean/1321.lean
new file mode 100644
index 0000000000..e2434ee03a
--- /dev/null
+++ b/tests/lean/1321.lean
@@ -0,0 +1,11 @@
+
+@[reducible] 
+syntax (name := fooParser) "foo" term : term
+
+#print fooParser
+
+macro_rules
+  | `(foo $x) => `($x + 1)
+
+#check foo 5
+
diff --git a/tests/lean/1321.lean.expected.out b/tests/lean/1321.lean.expected.out
new file mode 100644
index 0000000000..2b81ffa6ba
--- /dev/null
+++ b/tests/lean/1321.lean.expected.out
@@ -0,0 +1,4 @@
+@[reducible] def fooParser : Lean.ParserDescr :=
+Lean.ParserDescr.node `fooParser 1022
+  (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "foo") (Lean.ParserDescr.cat `term 0))
+5 + 1 : Nat