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

chore(kernel/expr): remove dead code

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-15 17:09:04 -08:00
parent 57e58c598c
commit c096eec1d6
2 changed files with 1 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/kernel/expr.cpp
View file

@ -279,16 +279,6 @@ bool is_arrow(expr const & t) {
} }
} }
bool is_heq(expr const & e, expr & lhs, expr & rhs) {
if (is_heq(e)) {
lhs = heq_lhs(e);
rhs = heq_rhs(e);
return true;
} else {
return false;
}
}
expr copy(expr const & a) { expr copy(expr const & a) {
switch (a.kind()) { switch (a.kind()) {
case expr_kind::Var: return mk_var(var_idx(a)); case expr_kind::Var: return mk_var(var_idx(a));
@ -465,7 +455,7 @@ public:
name n = read_name(d); name n = read_name(d);
return mk_metavar(n, read_local_context(d)); return mk_metavar(n, read_local_context(d));
}} }}
throw_corrupted_file(); throw_corrupted_file(); // LCOV_EXCL_LINE
}); });
} }
}; };

2
src/kernel/expr.h
View file

@ -544,8 +544,6 @@ inline name const & metavar_name(expr const & e) { return to_metavar(e)
inline local_context const & metavar_lctx(expr const & e) { return to_metavar(e)->get_lctx(); } inline local_context const & metavar_lctx(expr const & e) { return to_metavar(e)->get_lctx(); }
inline bool has_metavar(expr const & e) { return e.has_metavar(); } inline bool has_metavar(expr const & e) { return e.has_metavar(); }
bool is_heq(expr const & e, expr & lhs, expr & rhs);
// ======================================= // =======================================
// ======================================= // =======================================