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 2017-03-11 16:35:40 -08:00
parent d352ac4bcb
commit 9c24b81cbf
1 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1848,9 +1848,14 @@ expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<exp
if (is_choice(fn)) {
buffer<expr> fns;
if (amask != arg_mask::Default)
throw elaborator_exception(ref, "invalid explicit annotation, symbol is overloaded "
"(solution: use fully qualified names)");
if (amask != arg_mask::Default) {
format fmt = format("invalid explicit annotation because of overloading (possible solution: use fully qualified names) ");
for (unsigned i = 0; i < get_num_choices(fn); i++)
fns.push_back(get_choice(fn, i));
auto pp_fn = mk_pp_ctx();
fmt += pp_overloads(pp_fn, fns);
throw elaborator_exception(ref, fmt);
}
for (unsigned i = 0; i < get_num_choices(fn); i++) {
expr const & fn_i = get_choice(fn, i);
fns.push_back(fn_i);