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

fix(kernel/type_checker): typo

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-14 10:35:42 -07:00
parent 277e0e6d49
commit cf55a1bcc2
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/kernel/type_checker.cpp
View file

@ -209,7 +209,7 @@ struct type_checker::imp {
expr A_args = mk_app(A, args.size(), args.data());
args.push_back(Var(0));
expr B_args = mk_app(B, args.size(), args.data());
expr r = mk_pi(g_x_name, A, B);
expr r = mk_pi(g_x_name, A_args, B_args);
justification j = mk_justification(s,
[=](formatter const & fmt, options const & o, substitution const & subst) {
return pp_function_expected(fmt, m_env, o, subst.instantiate_metavars_wo_jst(s));