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

fix(library/unifier): typo

Browse source
This commit is contained in:
Leonardo de Moura 2015-03-12 13:15:23 -07:00
parent 3e4d849a4a
commit 8f004671a2
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/unifier.cpp
View file

@ -1630,7 +1630,7 @@ struct unifier_fn {
}
}
/** \brief Create the local context \c locals for the imitiation step.
/** \brief Create the local context \c locals for the imitation step.
*/
void mk_local_context(buffer<expr> & locals, constraint_seq & cs) {
expr mtype = mlocal_type(m);
@ -1654,7 +1654,7 @@ struct unifier_fn {
}
}
expr mk_imitiation_arg(expr const & arg, expr const & type, buffer<expr> const & locals,
expr mk_imitation_arg(expr const & arg, expr const & type, buffer<expr> const & locals,
constraint_seq & cs) {
// The following optimization is broken. It does not really work when we have dependent
// types. The problem is that the type of arg may depend on other arguments,
@ -1706,7 +1706,7 @@ struct unifier_fn {
for (expr const & rarg : rargs) {
f_type = tc().ensure_pi(f_type, cs);
expr d_type = binding_domain(f_type);
expr sarg = mk_imitiation_arg(rarg, d_type, locals, cs);
expr sarg = mk_imitation_arg(rarg, d_type, locals, cs);
sargs.push_back(sarg);
f_type = instantiate(binding_body(f_type), sarg);
}
@ -1731,7 +1731,7 @@ struct unifier_fn {
If f is a local constant, then we consider each a_i that is equal to f.
Remark: we try to minimize the number of constraints (?m_i a_1 ... a_k) =?= b_i by detecting "easy" cases
that can be solved immediately. See \c mk_imitiation_arg
that can be solved immediately. See \c mk_imitation_arg
*/
void mk_app_imitation() {
lean_assert(is_metavar(m));
@ -1780,13 +1780,13 @@ struct unifier_fn {
// create a scope to make sure no constraints "leak" into the current state
expr rhs_A = binding_domain(rhs);
expr A_type = tc().infer(rhs_A, cs);
expr A = mk_imitiation_arg(rhs_A, A_type, locals, cs);
expr A = mk_imitation_arg(rhs_A, A_type, locals, cs);
expr local = mk_local(u.m_ngen.next(), binding_name(rhs), A, binding_info(rhs));
locals.push_back(local);
margs.push_back(local);
expr rhs_B = instantiate(binding_body(rhs), local);
expr B_type = tc().infer(rhs_B, cs);
expr B = mk_imitiation_arg(rhs_B, B_type, locals, cs);
expr B = mk_imitation_arg(rhs_B, B_type, locals, cs);
expr binding = is_pi(rhs) ? Pi(local, B) : Fun(local, B);
locals.pop_back();
expr v = Fun(locals, binding);