chore: improve recovery tests

leanprover · Feb 20, 2024 · 253dda4 · 253dda4
1 parent c748682
commit 253dda4
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 3 deletions.
diff --git a/tests/lean/parserRecovery.lean b/tests/lean/parserRecovery.lean
@@ -18,9 +18,9 @@ def 5 : Nat := 3
 theorem yep : True := by trivial
 
 theorem () : Nat := 99
-theorem 2.4 : Nat := 99
-theorem "nat" : Nat := 99
-theorem 3 : Nat := 99
+theorem 2.4 : Nat := )
+theorem "nat" : Nat := )
+theorem 3 : Nat := )
 
 opaque ((( : Nat := )
 

diff --git a/tests/lean/parserRecovery.lean.expected.out b/tests/lean/parserRecovery.lean.expected.out
@@ -4,8 +4,11 @@ parserRecovery.lean:16:3-16:5: error: unexpected token; expected identifier
 parserRecovery.lean:20:7-20:9: error: unexpected token '('; expected identifier
 parserRecovery.lean:20:9-20:10: error: unexpected token ')'; expected '_' or identifier
 parserRecovery.lean:21:7-21:11: error: unexpected token; expected identifier
+parserRecovery.lean:21:20-21:22: error: unexpected token ')'; expected term
 parserRecovery.lean:22:7-22:13: error: unexpected token; expected identifier
+parserRecovery.lean:22:22-22:24: error: unexpected token ')'; expected term
 parserRecovery.lean:23:7-23:9: error: unexpected token; expected identifier
+parserRecovery.lean:23:18-23:20: error: unexpected token ')'; expected term
 parserRecovery.lean:25:6-25:8: error: unexpected token '('; expected identifier
 parserRecovery.lean:25:8-25:9: error: unexpected token '('; expected '_' or identifier
 parserRecovery.lean:27:5-27:12: error: unexpected token; expected identifier