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

fix(library/blast/infer_type): typos

Browse source
This commit is contained in:
Leonardo de Moura 2015-10-16 17:32:40 -07:00
parent 13ccbaa0d9
commit ee924e4842
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/blast/infer_type.cpp
View file

@ -368,7 +368,7 @@ static bool assign_mref_core(expr const & ma, expr const & v) {
s.assign_mref(m, new_v);
return true;
} else if (args.size() == locals.size()) {
s.assign_mref(m, Fun(locals, v));
s.assign_mref(m, Fun(locals, new_v));
return true;
} else {
// This case is imprecise since it is not a higher order pattern.
@ -386,7 +386,7 @@ static bool assign_mref_core(expr const & ma, expr const & v) {
m_type = instantiate(binding_body(m_type), locals[i]);
}
lean_assert(locals.size() == args.size());
s.assign_mref(m, Fun(locals, v));
s.assign_mref(m, Fun(locals, new_v));
return true;
}
}