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

chore(frontends/lean/parser): remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-11 16:29:58 -08:00
parent 04e92e1e96
commit 30d20e8029
2 changed files with 0 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/frontends/lean/parser.cpp
View file

@ -354,19 +354,6 @@ expr parser::copy_with_new_pos(expr const & e, pos_info p) {
lean_unreachable(); // LCOV_EXCL_LINE
}
/** \brief Add \c ls to constants occurring in \c e. */
expr parser::propagate_levels(expr const & e, levels const & ls) {
if (is_nil(ls)) {
return e;
} else {
return replace(e, [&](expr const & e) {
if (is_constant(e))
return some_expr(update_constant(e, ls));
return none_expr();
});
}
}
pos_info parser::pos_of(expr const & e, pos_info default_pos) const {
tag t = e.get_tag();
if (t == nulltag)

1
src/frontends/lean/parser.h
View file

@ -164,7 +164,6 @@ class parser {
tag get_tag(expr e);
expr copy_with_new_pos(expr const & e, pos_info p);
expr propagate_levels(expr const & e, levels const & ls);
cmd_table const & cmds() const { return get_cmd_table(env()); }
parse_table const & nud() const { return get_nud_table(env()); }