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

fix(library/compiler/emit_cpp): missing enf_unreachable case

Browse source
This commit is contained in:
Leonardo de Moura 2019-01-31 16:36:37 -08:00
parent 4166851574
commit 5f29b1003b
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -173,7 +173,7 @@ static void emit_fn_decl(std::ostream & out, environment const & env, name const
/* Auxiliary function for `collect_dependencies`. */
static void collect_constant(expr const & e, name_set & deps) {
lean_assert(is_constant(e));
if (!is_llnf_op(e) && !is_builtin_constant(const_name(e)) && e != mk_enf_neutral()) {
if (!is_llnf_op(e) && !is_builtin_constant(const_name(e)) && !is_enf_neutral(e) && !is_enf_unreachable(e)) {
deps.insert(const_name(e));
}
}
@ -711,8 +711,8 @@ public:
void operator()(comp_decl const & d) {
name n = d.fst();
expr type = get_constant_ll_type(m_env, n);
expr e = d.snd();
expr type = get_constant_ll_type(m_env, n);
m_out << to_cpp_type(get_result_type(type)) << " ";
if (is_lambda(e)) {
buffer<expr> locals;