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

feat(frontends/lean/elaborator): improve error message

Browse source
This commit is contained in:
Leonardo de Moura 2016-09-03 11:37:53 -07:00
parent a60f4e2699
commit 3bc5cf8d0e
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/elaborator.cpp
View file

@ -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);