michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/coercion): improve error message when coercion has no viable source

Browse source
This commit is contained in:
Daniel Selsam 2015-08-13 21:24:33 -07:00 • committed by Leonardo de Moura
parent 5bef45b1fd
commit 7223293a93
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/coercion.cpp
View file

@ -366,7 +366,9 @@ environment add_coercion(environment const & env, io_state const &, name const &
t = binding_body(t); t = binding_body(t);
} }
if (Cs.empty()) if (Cs.empty())
throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion"); throw exception(sstream() << "invalid coercion, '" << f << "' cannot be used as a coercion "
<< "because there is no acceptable source type; coercions must be of the form\n"
<< "coe : Pi (x_1 : A_1) ... (x_n : A_n) (y: C x_1 ... x_n), <target>");
unsigned i = Cs.size(); unsigned i = Cs.size();
while (i > 0) { while (i > 0) {
--i; --i;