From 98b4e09063ace0b0fe20c46f70e40c28b49cd98c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Sep 2013 22:09:08 -0700 Subject: [PATCH] refactor(kernel): simplify expr_eq Signed-off-by: Leonardo de Moura --- src/kernel/expr_eq.h | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/src/kernel/expr_eq.h b/src/kernel/expr_eq.h index 1829e4c57..f2b480ea2 100644 --- a/src/kernel/expr_eq.h +++ b/src/kernel/expr_eq.h @@ -56,14 +56,7 @@ class expr_eq_fn { case expr_kind::Pi: return apply(abst_domain(a), abst_domain(b)) && apply(abst_body(a), abst_body(b)); case expr_kind::Type: return ty_level(a) == ty_level(b); case expr_kind::Value: return to_value(a) == to_value(b); - case expr_kind::Let: - if (let_type(a) && let_type(b)) { - if (!apply(let_type(a), let_type(b))) - return false; - } else if (let_type(a) || let_type(b)) { - return false; - } - return apply(let_value(a), let_value(b)) && apply(let_body(a), let_body(b)); + case expr_kind::Let: return apply(let_type(a), let_type(b)) && apply(let_value(a), let_value(b)) && apply(let_body(a), let_body(b)); case expr_kind::MetaVar: return metavar_idx(a) == metavar_idx(b) && compare(metavar_ctx(a), metavar_ctx(b), [&](meta_entry const & e1, meta_entry const & e2) {