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

feat(library/compiler/erase_irrelevant): add support for lc_unreachable

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-30 08:25:06 -07:00
parent 2c4139d5e5
commit a17b95acc7
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/compiler/erase_irrelevant.cpp
View file

@ -82,6 +82,8 @@ class erase_irrelevant_fn : public compiler_step_visitor {
virtual expr visit_constant(expr const & e) override {
if (is_comp_irrelevant(e)) {
return *g_neutral_expr;
} else if (const_name(e) == get_lc_unreachable_name()) {
return *g_unreachable_expr;
} else {
/* Erase universe level information */
return mk_constant(const_name(e));
@ -395,6 +397,8 @@ class erase_irrelevant_fn : public compiler_step_visitor {
return visit_subtype_mk(args);
} else if (n == get_subtype_val_name()) {
return visit_subtype_val(args);
} else if (n == get_lc_unreachable_name()) {
return *g_unreachable_expr;
}
}
return compiler_step_visitor::visit_app(e);