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

chore(library/app_builder): fix typo in trace message

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-03 15:16:50 -08:00
parent d0fe59ef8a
commit fcf532ea67
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/app_builder.cpp
View file

@ -268,7 +268,7 @@ struct app_builder::imp {
lean_trace("app_builder", lean_trace("app_builder",
trace_fun(n); trace_fun(n);
tout () << ", failed to solve unification constraint for #" << (i+1) tout () << ", failed to solve unification constraint for #" << (i+1)
<< "argument (" << m_ctx->infer(m) << " =?= " << m_ctx->infer(v) << ")\n";); << " argument (" << m_ctx->infer(m) << " =?= " << m_ctx->infer(v) << ")\n";);
} }
expr mk_app(name const & c, unsigned nargs, expr const * args) { expr mk_app(name const & c, unsigned nargs, expr const * args) {