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

fix(library/blast/subst_action): missing occurs check

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-02 22:51:03 -08:00
parent d2054bb65c
commit acb5b969c6
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/blast/subst_action.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "library/occurs.h"
#include "library/blast/revert.h"
#include "library/blast/intros_action.h"
#include "library/blast/blast.h"
@ -98,9 +99,9 @@ action_result subst_action(hypothesis_idx hidx) {
expr lhs, rhs;
if (!is_eq(type, lhs, rhs))
return action_result::failed();
if (is_href(rhs)) {
if (is_href(rhs) && !occurs(rhs, lhs)) {
return action_result(subst_core(hidx));
} else if (is_href(lhs)) {
} else if (is_href(lhs) && !occurs(lhs, rhs)) {
if (s.has_forward_deps(href_index(lhs))) {
// TODO(Leo): we don't handle this case yet.
// Other hypotheses depend on this equality.