From abbc48324629ab3dc4a180cd98c2a3cfbdb36f7e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 12 Mar 2017 16:48:14 -0700 Subject: [PATCH] chore(tests/lean/type_error_at_eval_expr): fix test We should suppress the internal numerical ids when displaying this kind of error message as suggested by @kha --- tests/lean/type_error_at_eval_expr.lean.expected.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/lean/type_error_at_eval_expr.lean.expected.out b/tests/lean/type_error_at_eval_expr.lean.expected.out index 5f17e591af..de19830752 100644 --- a/tests/lean/type_error_at_eval_expr.lean.expected.out +++ b/tests/lean/type_error_at_eval_expr.lean.expected.out @@ -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 ℕ