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

chore(frontends/lean/elaborator): improve error positions

Browse source
This commit is contained in:
Sebastian Ullrich 2018-11-19 15:28:23 +01:00
parent 774d776133
commit 7d7d15f8f7
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2003,6 +2003,7 @@ expr elaborator::visit_app(expr const & e, optional<expr> const & expected_type)
return visit_scope_trace(e, expected_type);
buffer<expr> args;
expr const & fn = get_app_args(e, args);
flet<optional<pos_info>> _(m_last_pos, get_pos(fn));
expr ufn = unwrap_pos(fn);
if (is_infix_function(ufn)) {
expr infix_fn = get_annotation_arg(ufn);