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

fix(library/elaborator): missing condition

Browse source 
The elaborator was failing in the following higher-order constraint

   ctx |- (?M a) = (?M b)

This constraint has solution, but the missing condition was making the elaborator to reduce this problem to

   ctx |- a = b

That does not have a solution.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-15 14:11:33 -08:00
parent f67b5c4d00
commit f177c8d1ec
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1354,7 +1354,7 @@ class elaborator::imp {
if (process_assigned_metavar(c, a, true) || process_assigned_metavar(c, b, false))
return true;
if (m_assume_injectivity && is_app(a) && is_app(b) && num_args(a) == num_args(b) && arg(a, 0) == arg(b, 0)) {
if (m_assume_injectivity && is_app(a) && is_app(b) && num_args(a) == num_args(b) && arg(a, 0) == arg(b, 0) && !is_metavar(arg(a, 0))) {
// If m_assume_injectivity is true, we apply the following rule
// ctx |- (f a1 a2) == (f b1 b2)
// ===>