From 79acd3e1b7272d5a33a94d4cd5a4d413a1222a1d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 28 Aug 2014 15:21:57 -0700 Subject: [PATCH] fix(kernel/converter): missing case Signed-off-by: Leonardo de Moura --- src/kernel/converter.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp index babbb7d82..5c8b17304 100644 --- a/src/kernel/converter.cpp +++ b/src/kernel/converter.cpp @@ -200,7 +200,7 @@ struct default_converter : public converter { lean_assert(m <= num_args); r = whnf_core(mk_rev_app(instantiate(binding_body(f), m, args.data() + (num_args - m)), num_args - m, args.data()), c); } else { - r = is_eqp(f, f0) ? e : mk_rev_app(f, args.size(), args.data()); + r = f == f0 ? e : whnf_core(mk_rev_app(f, args.size(), args.data()), c); } break; }} @@ -466,6 +466,7 @@ struct default_converter : public converter { // apply whnf (without using delta-reduction or normalizer extensions) expr t_n = whnf_core(t, c); expr s_n = whnf_core(s, c); + if (!is_eqp(t_n, t) || !is_eqp(s_n, s)) { r = quick_is_def_eq(t_n, s_n, c, jst, cs); if (r != l_undef) return to_bcs(r == l_true, cs);