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

fix(library/unifier): set conflict if type mismatch during metavariable assignment

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-25 09:33:34 -07:00
parent 5b6589709c
commit 18a883ab1b
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/unifier.cpp
View file

@ -457,8 +457,12 @@ struct unifier_fn {
m_subst = m_subst.assign(m, v, j);
expr m_type = mlocal_type(m);
expr v_type = m_tc.infer(v);
if (in_conflict() || !m_tc.is_def_eq(m_type, v_type, j))
if (in_conflict())
return false;
if (!m_tc.is_def_eq(m_type, v_type, j)) {
set_conflict(j);
return false;
}
auto it = m_mvar_occs.find(mlocal_name(m));
if (it) {
cnstr_idx_set s = *it;