From cd3bbb1ebf66f04e82a9853670e05635c76bcc44 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 31 Dec 2013 10:14:17 -0800 Subject: [PATCH] fix(kernel/builtin): enforcing design decision: semantic attachments are NOT simplifiers, they should do only evaluation Signed-off-by: Leonardo de Moura --- src/kernel/builtin.cpp | 2 +- tests/lean/tst10.lean.expected.out | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index 1a3a53ef8c..a0b2d260b3 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -101,7 +101,7 @@ public: virtual expr get_type() const { return m_type; } virtual name get_name() const { return g_if_name; } virtual optional normalize(unsigned num_args, expr const * args) const { - if (num_args == 5 && is_bool_value(args[2])) { + if (num_args == 5 && is_bool_value(args[2]) && is_value(args[3]) && is_value(args[4])) { if (to_bool(args[2])) return some_expr(args[3]); // if A true a b --> a else diff --git a/tests/lean/tst10.lean.expected.out b/tests/lean/tst10.lean.expected.out index 5ba3288e85..f57a72c9ae 100644 --- a/tests/lean/tst10.lean.expected.out +++ b/tests/lean/tst10.lean.expected.out @@ -16,7 +16,7 @@ a ∨ a ∨ b a ⇒ b ⇒ a a ⇒ b : Bool if a a ⊤ -a +if ⊤ a ⊤ Assumed: H1 Assumed: H2 @MP : Π (a b : Bool), (a ⇒ b) → a → b