chore: add parser tests

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

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