From 63434fbb7d0723c51ac7559fef3e9b10ebc3267f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 4 Feb 2020 10:11:50 -0800
Subject: [PATCH] chore: add parser tests

---
 tests/lean/precissues.lean              | 31 +++++++++++++++++++++++++
 tests/lean/precissues.lean.expected.out | 17 ++++++++++++++
 2 files changed, 48 insertions(+)
 create mode 100644 tests/lean/precissues.lean
 create mode 100644 tests/lean/precissues.lean.expected.out

diff --git a/tests/lean/precissues.lean b/tests/lean/precissues.lean
new file mode 100644
index 0000000000..b2bd418e12
--- /dev/null
+++ b/tests/lean/precissues.lean
@@ -0,0 +1,31 @@
+new_frontend
+
+#check id fun x => x -- should fail
+
+def f (x : Nat) (g : Nat → Nat) := g x
+
+#check f 1 fun x => x -- should fail
+
+#check f 1 (fun x => x)
+
+#check id have True from ⟨⟩; this -- should fail
+
+#check 1
+
+#check id (have True from ⟨⟩; this)
+
+#check 0 = have Nat from 1; this
+#check 0 = let x := 0; x
+
+variables (p q r : Prop)
+macro_rules `(¬ $p) => `(Not $p)
+
+#check p ↔ ¬ q
+#check True = ¬ False
+#check p ∧ ¬q
+#check ¬p ∧ q
+#check ¬p ↔ q
+#check ¬(p = q)
+#check ¬ p = q
+#check id ¬p
+#check Nat → ∀ (a : Nat), a = a
diff --git a/tests/lean/precissues.lean.expected.out b/tests/lean/precissues.lean.expected.out
new file mode 100644
index 0000000000..88f363bd7a
--- /dev/null
+++ b/tests/lean/precissues.lean.expected.out
@@ -0,0 +1,17 @@
+precissues.lean:3:10: error: unexpected token; expected longestMatch: empty list or '('
+precissues.lean:7:11: error: unexpected token; expected longestMatch: empty list or '('
+f 1 (λ (x : Nat), x) : Nat
+precissues.lean:11:10: error: unexpected token; expected longestMatch: empty list or '('
+1 : Nat
+id ((λ (this : True), this) True.intro) : True
+0=(λ (this : Nat), this) 1 : Prop
+0=let x : Nat := 0 in x : Prop
+p↔¬q : Prop
+True=¬False : Prop
+p∧¬q : Prop
+¬p∧q : Prop
+¬p↔q : Prop
+¬p=q : Prop
+¬p=q : Prop
+id (¬p) : Prop
+Nat → ∀ (a : Nat), a=a : Prop