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

chore(library/tactic/congruence/congruence_closure): remove unnecessary field

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-24 09:14:25 -08:00
parent 0906d84c92
commit 8f401c8752
2 changed files with 1 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/tactic/congruence/congruence_closure.cpp
View file

@ -119,9 +119,6 @@ static optional<ext_congr_lemma> mk_hcongr_lemma_core(type_context & ctx, expr c
ext_congr_lemma res1(*eq_congr);
expr type = eq_congr->get_type();
while (is_pi(type)) type = binding_body(type);
/* If all arguments are Eq kind, then we can use generic congr axiom and consider equality for the function. */
if (!is_heq(type) && eq_congr->all_eq_kind())
res1.m_fixed_fun = false;
lean_assert(is_eq(type) || is_heq(type));
res1.m_hcongr_lemma = true;
if (is_heq(type))

6
src/library/tactic/congruence/congruence_closure.h
View file

@ -246,17 +246,13 @@ public:
struct ext_congr_lemma {
/* The basic congr_lemma object defined at congr_lemma_manager */
congr_lemma m_congr_lemma;
/* If m_fixed_fun is false, then we build equivalences for functions,
and use generic congr lemma, and ignore m_congr_lemma.
That is, even the function can be treated as an Eq argument. */
unsigned m_fixed_fun:1;
/* If m_heq_result is true, then lemma is based on heterogeneous equality
and the conclusion is a heterogeneous equality. */
unsigned m_heq_result:1;
/* If m_heq_lemma is true, then lemma was created using mk_hcongr_lemma. */
unsigned m_hcongr_lemma:1;
ext_congr_lemma(congr_lemma const & H):
m_congr_lemma(H), m_fixed_fun(true), m_heq_result(false), m_hcongr_lemma(false) {}
m_congr_lemma(H), m_heq_result(false), m_hcongr_lemma(false) {}
};
void initialize_congruence_closure();