chore(tests): add demo for parser error recovery

This commit is contained in:
Gabriel Ebner 2017-05-19 18:53:21 +02:00 committed by Leonardo de Moura
parent 6b956ad658
commit 8bd09fe282
2 changed files with 31 additions and 0 deletions

View file

@ -0,0 +1,21 @@
/- unknown identifiers -/
def f1 :
| 42 := 9000
| arg := ag
#eval f1 42 -- OK (prints 9000)
/- incomplete structure instances -/
def f2 : × := { fst := 9000, sn}
#reduce f2.fst -- OK (prints 9000)
/- incomplete if-then-else -/
def f3 (x : ) : :=
(if x ≥ 42 then 9000)
-- ^ missing else reported here
#eval f3 42 -- OK (prints 9000)

View file

@ -0,0 +1,10 @@
parser_error_recovery.lean:5:9: error: unknown identifier 'ag'
parser_error_recovery.lean:3:0: warning: declaration 'f1' uses sorry
9000
parser_error_recovery.lean:11:35: error: invalid structure instance, ':=' expected
parser_error_recovery.lean:11:18: error: invalid structure value { ... }, field 'snd' was not provided
parser_error_recovery.lean:11:18: error: invalid structure value { ... }, 'sn' is not a field of structure 'prod'
9000
parser_error_recovery.lean:18:20: error: invalid 'if-then-else' expression, 'else' expected
parser_error_recovery.lean:17:0: warning: declaration 'f3' uses sorry
9000