From b70edfaa2d42fa6cebbecbb5cdc5f1de7a69872a Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 11 Dec 2019 14:44:39 +0100
Subject: [PATCH] test: simple quotation terms

---
 tests/lean/StxQuot.lean              | 13 +++++++++++++
 tests/lean/StxQuot.lean.expected.out |  4 ++++
 2 files changed, 17 insertions(+)
 create mode 100644 tests/lean/StxQuot.lean
 create mode 100644 tests/lean/StxQuot.lean.expected.out

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)))"