From b444756d20675800d7a2881f3c0f7a34085e042f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Jan 2014 22:14:01 -0800 Subject: [PATCH] fix(library/simplifier): missing condition in implication simplification Signed-off-by: Leonardo de Moura --- src/library/simplifier/simplifier.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index 784045787..47a557fee 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -1418,7 +1418,7 @@ class simplifier_cell::imp { result simplify_pi(expr const & e) { lean_assert(is_pi(e)); if (is_arrow(e)) { - if (is_proposition(abst_domain(e))) + if (is_proposition(abst_domain(e)) && is_proposition(abst_body(e))) return simplify_implication(e); else return simplify_arrow(e);