chore: fix some tests

tests/lean/appParserIssue.lean

@@ -9,5 +9,5 @@ new_frontend
 syntax "foo" term:max term:max : term
 macro_rules `(foo $x $y) => `(f $x $y)
 
-#check foo 1 fun x => x   -- should fail?
 #check foo 1 (fun x => x) -- should work
+#check foo 1 fun x => x   -- should fail?

tests/lean/appParserIssue.lean.expected.out

@@ -2,5 +2,4 @@ f 1 : (Nat → Nat) → Nat
 appParserIssue.lean:5:11: error: expected command
 f 1 (λ (x : Nat), x) : Nat
 f 1 (λ (x : Nat), x) : Nat
-appParserIssue.lean:12:13: error: unexpected token at this precedence level; consider parenthesizing the term
-f 1 (λ (x : Nat), x) : Nat
+appParserIssue.lean:13:13: error: unexpected token at this precedence level; consider parenthesizing the term

tests/lean/precissues.lean

@@ -2,10 +2,14 @@ new_frontend
 
 #check id fun x => x -- should fail
 
+#check 0
+
 def f (x : Nat) (g : Nat → Nat) := g x
 
 #check f 1 fun x => x -- should fail
 
+#check 0
+
 #check f 1 (fun x => x)
 
 #check id have True from ⟨⟩; this -- should fail

tests/lean/precissues.lean.expected.out

@@ -1,11 +1,10 @@
 id : ?m_1 → ?m_1
 precissues.lean:3:10: error: expected command
 f 1 : (Nat → Nat) → Nat
-precissues.lean:7:11: error: expected command
+precissues.lean:9:11: error: expected command
 f 1 (λ (x : Nat), x) : Nat
 id : ?m_1 → ?m_1
-precissues.lean:11:10: error: expected command
-1 : Nat
+precissues.lean:15:10: error: expected command
 id ((λ (this : True), this) True.intro) : True
 0=(λ (this : Nat), this) 1 : Prop
 0=let x : Nat := 0 in x : Prop

tests/lean/run/macro.lean

@@ -6,7 +6,7 @@ axiom mem {α : Type} : α → Set α → Prop
 axiom univ {α : Type} : Set α
 axiom Union {α : Type} : Set (Set α) → Set α
 
-syntax term " ∈ ":100 term:99 : term
+syntax:100 term " ∈ " term:99 : term
 
 macro_rules
 | `($x ∈ $s) => `(mem $x $s)

tests/lean/run/termParserAttr.lean

@@ -13,7 +13,7 @@ do env  ← MetaIO.getEnv;
 
 open Lean.Parser
 
-@[termParser] def tst := parser! "(|" >> termParser >> optional (symbolAux ", " >> termParser) >> "|)"
+@[termParser] def tst := parser! "(|" >> termParser >> optional (symbol ", " >> termParser) >> "|)"
 
 @[termParser] def boo : ParserDescr :=
 ParserDescr.node `boo