From 434c148800af022e59bb878173208fbe4af26bd3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 1 Jan 2020 14:16:49 -0800
Subject: [PATCH] test: add `termElab` attribute test

---
 tests/lean/run/termParserAttr.lean   | 36 ++++++++++++++++++++++++++++
 tests/playground/termParserAttr.lean |  6 ++++-
 2 files changed, 41 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/termParserAttr.lean

diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean
new file mode 100644
index 0000000000..0d509672c5
--- /dev/null
+++ b/tests/lean/run/termParserAttr.lean
@@ -0,0 +1,36 @@
+import Init.Lean
+open Lean
+open Lean.Elab
+
+def run (input : String) (failIff : Bool := true) : MetaIO Unit :=
+do env  ← MetaIO.getEnv;
+   opts ← MetaIO.getOptions;
+   let (env, messages) := process input env opts;
+   messages.toList.forM $ fun msg => IO.println msg;
+   when (failIff && messages.hasErrors) $ throw (IO.userError "errors have been found");
+   when (!failIff && !messages.hasErrors) $ throw (IO.userError "there are no errors");
+   pure ()
+
+open Lean.Parser
+@[termParser] def tst := parser! "(|" >> termParser >> "|)"
+
+@[termParser] def boo : ParserDescr :=
+ParserDescr.node `boo
+  (ParserDescr.andthen
+    (ParserDescr.symbol "[|" 0)
+    (ParserDescr.andthen
+      (ParserDescr.parser `term 0)
+      (ParserDescr.symbol "|]" 0)))
+
+open Lean.Elab.Term
+
+@[termElab tst] def elabTst : TermElab :=
+fun stx expected? =>
+  elabTerm (stx.getArg 1) expected?
+
+@[termElab boo] def elabBoo : TermElab :=
+fun stx expected? =>
+  elabTerm (stx.getArg 1) expected?
+
+#eval run "#check [| @id.{1} Nat |]"
+#eval run "#check (| id 1 |)"
diff --git a/tests/playground/termParserAttr.lean b/tests/playground/termParserAttr.lean
index 6c71eecd75..0d509672c5 100644
--- a/tests/playground/termParserAttr.lean
+++ b/tests/playground/termParserAttr.lean
@@ -28,5 +28,9 @@ open Lean.Elab.Term
 fun stx expected? =>
   elabTerm (stx.getArg 1) expected?
 
+@[termElab boo] def elabBoo : TermElab :=
+fun stx expected? =>
+  elabTerm (stx.getArg 1) expected?
+
 #eval run "#check [| @id.{1} Nat |]"
--- #eval run "#check (| id 1 |)"
+#eval run "#check (| id 1 |)"