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

fix(kernel/builtin): enforcing design decision: semantic attachments are NOT simplifiers, they should do only evaluation

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-31 10:14:17 -08:00
parent c485b4bc4c
commit cd3bbb1ebf
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/builtin.cpp
View file

@ -101,7 +101,7 @@ public:
virtual expr get_type() const { return m_type; }
virtual name get_name() const { return g_if_name; }
virtual optional<expr> 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

2
tests/lean/tst10.lean.expected.out
View file

@ -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