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

chore(kernel/default_converter): remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-13 13:33:13 -08:00
parent 8fded5224b
commit 723a9e227a
2 changed files with 0 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/kernel/default_converter.cpp
View file

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

1
src/kernel/default_converter.h
View file

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