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

fix(library/elaborator): temporary fix for bug reported by Jeremy

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-02-24 15:26:21 -08:00
parent 16844fff73
commit 309e7ba880
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/elaborator/elaborator.cpp
View file

@ -1727,6 +1727,11 @@ class elaborator::imp {
if (!eq && is_bool(a) && is_type(b)) if (!eq && is_bool(a) && is_type(b))
return true; return true;
if ((is_proj(a) && instantiate_metavars(true, a, c)) ||
(is_proj(b) && instantiate_metavars(false, b, c))) {
return true;
}
if (a.kind() == b.kind()) { if (a.kind() == b.kind()) {
switch (a.kind()) { switch (a.kind()) {
case expr_kind::Constant: case expr_kind::Var: case expr_kind::Value: case expr_kind::Constant: case expr_kind::Var: case expr_kind::Value: