From 3bc5cf8d0e89e10af6d2cc32405ef456e1ec7759 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 3 Sep 2016 11:37:53 -0700 Subject: [PATCH] feat(frontends/lean/elaborator): improve error message --- src/frontends/lean/elaborator.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 631bc1d3f9..5631f08f10 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2027,7 +2027,8 @@ expr_pair elaborator::elaborate_with_type(expr const & e, expr const & e_type) { } else { auto pp_fn = mk_pp_ctx(); throw elaborator_exception(ref, - format("type mismatch, expression has type") + pp_indent(pp_fn, inferred_type) + + format("type mismatch, expression") + pp_indent(pp_fn, new_e) + + line() + format("has type") + pp_indent(pp_fn, inferred_type) + line() + format("but is expected to have type") + pp_indent(pp_fn, new_e_type)); } return mk_pair(new_e, new_e_type);