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

feat(library/type_context): add new trace msg

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-03 15:32:04 -07:00
parent bf730d992c
commit c32138db88
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/type_context.cpp
View file

@ -1461,6 +1461,10 @@ optional<expr> type_context::check_assignment(buffer<expr> const & locals, expr
if (std::all_of(locals.begin(), locals.end(), [&](expr const & a) {
return mlocal_name(a) != mlocal_name(e); })) {
ok = false;
lean_trace(name({"type_context", "is_def_eq_detail"}),
tout() << "failed to assign " << mvar << " to\n" << v << "\n" <<
"value contains local declaration " << e <<
" which is not in the scope of the metavariable";);
return false;
}
}