max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/compiler/rec_fn_macro): remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2018-05-30 13:16:34 -07:00
parent 1a369521cb
commit 843cd9bacb
2 changed files with 0 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/compiler/rec_fn_macro.cpp
View file

@ -78,11 +78,6 @@ name const & get_rec_fn_name(expr const & e) {
return static_cast<rec_fn_macro_definition_cell const*>(macro_def(e).raw())->get_rec_fn_name();
}
expr const & get_rec_fn_type(expr const & e) {
lean_assert(is_rec_fn_macro(e));
return macro_arg(e, 0);
}
void initialize_rec_fn_macro() {
g_rec_fn_macro_id = new name("rec_fn");
g_rec_fn_opcode = new std::string("RecFn");

1
src/library/compiler/rec_fn_macro.h
View file

@ -16,7 +16,6 @@ expr mk_rec_fn_macro(name const & fn_name, expr const & type);
bool is_rec_fn_macro(expr const & e);
name const & get_rec_fn_name(expr const & e);
expr const & get_rec_fn_type(expr const & e);
void initialize_rec_fn_macro();
void finalize_rec_fn_macro();