From 8f401c875285e6aed3a79e916f772ca5fe26780a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 24 Dec 2016 09:14:25 -0800 Subject: [PATCH] chore(library/tactic/congruence/congruence_closure): remove unnecessary field --- src/library/tactic/congruence/congruence_closure.cpp | 3 --- src/library/tactic/congruence/congruence_closure.h | 6 +----- 2 files changed, 1 insertion(+), 8 deletions(-) diff --git a/src/library/tactic/congruence/congruence_closure.cpp b/src/library/tactic/congruence/congruence_closure.cpp index e1b74ec7ea..74331e38fa 100644 --- a/src/library/tactic/congruence/congruence_closure.cpp +++ b/src/library/tactic/congruence/congruence_closure.cpp @@ -119,9 +119,6 @@ static optional 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)) diff --git a/src/library/tactic/congruence/congruence_closure.h b/src/library/tactic/congruence/congruence_closure.h index 84824c13bf..90a4a66c9e 100644 --- a/src/library/tactic/congruence/congruence_closure.h +++ b/src/library/tactic/congruence/congruence_closure.h @@ -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();