max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/unifier): bug in mk_imitiation_arg

Browse source 
Remove bogus constraint
     cs.push_back(mk_eq_cnstr(mk_app(maux_type, locals), type, j, relax));
This constraint is incorrect because 'type' may contain local constants that are not in 'locals'.

We just rely on
   cs.push_back(mk_eq_cnstr(mk_app(maux, margs), arg, j, relax));
When maux is assigned, the system will inforce that its type (which is based on maux_type) must be type correct

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-11 14:35:39 -07:00
parent cb8185f016
commit d47d326cef
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/unifier.cpp
View file

@ -1453,7 +1453,6 @@ struct unifier_fn {
} else {
expr maux_type = mk_metavar(u.m_ngen.next(), Pi(locals, mk_sort(mk_meta_univ(u.m_ngen.next()))));
expr maux = mk_metavar(u.m_ngen.next(), Pi(locals, mk_app(maux_type, locals)));
cs.push_back(mk_eq_cnstr(mk_app(maux_type, locals), type, j, relax));
cs.push_back(mk_eq_cnstr(mk_app(maux, margs), arg, j, relax));
return mk_app(maux, locals);
}