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

fix(library/definitional/equations): typo and bug

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-03 15:29:34 -08:00
parent 5bf8141af2
commit 376126241e
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/definitional/equations.cpp
View file

@ -867,7 +867,7 @@ class equation_compiler_fn {
/** \brief Return true iff \c t1 and \c t2 are instances of the same inductive datatype */
static bool is_same_inductive(expr const & t1, expr const & t2) {
return const_name(get_app_fn(t1)) != const_name(get_app_fn(t2));
return const_name(get_app_fn(t1)) == const_name(get_app_fn(t2));
}
/** \brief Return true iff \c s is structurally smaller than \c t OR equal to \c t */
@ -929,6 +929,8 @@ class equation_compiler_fn {
// arg_j must be structurally smaller than arg
if (!m_main.is_lt(arg_j, arg))
return false;
} else {
return false;
}
break;
}