diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean
new file mode 100644
index 0000000000..4227879484
--- /dev/null
+++ b/tests/lean/StxQuot.lean
@@ -0,0 +1,13 @@
+import Init.Lean
+
+namespace Lean
+open Lean.Elab
+
+def run : Unhygienic Syntax → String := toString ∘ Unhygienic.run
+
+#eval run `(Nat.one)
+#eval run `(1 + 1)
+#eval run $ do a ← `(Nat.one); `(%%a)
+#eval run $ do a ← `(Nat.one); `(f %%(id a))
+
+end Lean
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
new file mode 100644
index 0000000000..e88fa0a4d0
--- /dev/null
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -0,0 +1,4 @@
+"(Term.id `Nat.one (null))"
+"(Term.add (numLit \"1\") \"+\" (numLit \"1\"))"
+"(Term.id `Nat.one (null))"
+"(Term.app (Term.id `f (null)) (Term.id `Nat.one (null)))"