max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(tests/lean/type_error_at_eval_expr): fix test

Browse source 
We should suppress the internal numerical ids when displaying this kind
of error message as suggested by @kha
This commit is contained in:
Leonardo de Moura 2017-03-12 16:48:14 -07:00
parent 8d409d7c63
commit abbc483246
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/type_error_at_eval_expr.lean.expected.out
View file

@ -1,6 +1,6 @@
type_error_at_eval_expr.lean:3:0: error: eval_expr failed due to type error
nested exception message:
type mismatch at definition '_eval_expr.16.436', has type
type mismatch at definition '_eval_expr.16.439', has type
list ℕ
but is expected to have type
ℕ