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