From 723a9e227a3ed267a260f094dbf81316ca7349ba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 13 Jan 2016 13:33:13 -0800 Subject: [PATCH] chore(kernel/default_converter): remove dead code --- src/kernel/default_converter.cpp | 6 ------ src/kernel/default_converter.h | 1 - 2 files changed, 7 deletions(-) diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp index ca561a0db..a24a8aefa 100644 --- a/src/kernel/default_converter.cpp +++ b/src/kernel/default_converter.cpp @@ -322,12 +322,6 @@ bool default_converter::is_def_eq_args(expr t, expr s, constraint_seq & cs) { return !is_app(t) && !is_app(s); } -/** \brief Return true iff t is a constant named f_name or an application of the form (f_name a_1 ... a_k) */ -bool default_converter::is_app_of(expr t, name const & f_name) { - t = get_app_fn(t); - return is_constant(t) && const_name(t) == f_name; -} - /** \brief Try to solve (fun (x : A), B) =?= s by trying eta-expansion on s */ bool default_converter::try_eta_expansion_core(expr const & t, expr const & s, constraint_seq & cs) { if (is_lambda(t) && !is_lambda(s)) { diff --git a/src/kernel/default_converter.h b/src/kernel/default_converter.h index 2adb118c9..ac91a6d21 100644 --- a/src/kernel/default_converter.h +++ b/src/kernel/default_converter.h @@ -61,7 +61,6 @@ protected: lbool quick_is_def_eq(expr const & t, expr const & s, constraint_seq & cs, bool use_hash = false); bool is_def_eq_args(expr t, expr s, constraint_seq & cs); - bool is_app_of(expr t, name const & f_name); bool try_eta_expansion_core(expr const & t, expr const & s, constraint_seq & cs); bool try_eta_expansion(expr const & t, expr const & s, constraint_seq & cs) { return try_eta_expansion_core(t, s, cs) || try_eta_expansion_core(s, t, cs);