diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp index b4bd8a891b..9119abda81 100644 --- a/src/library/compiler/vm_compiler.cpp +++ b/src/library/compiler/vm_compiler.cpp @@ -211,6 +211,8 @@ class vm_compiler_fn { } else if (is_constant(fn)) { if (is_neutral_expr(fn)) { emit(mk_sconstructor_instr(0)); + } else if (is_unreachable_expr(fn)) { + emit(mk_unreachable_instr()); } else if (optional decl = get_vm_decl(m_env, const_name(fn))) { compile_global(*decl, args.size(), args.data(), bpz, m); } else { diff --git a/tests/lean/macro1.lean.expected.out b/tests/lean/macro1.lean.expected.out index 09606ab61c..e48c71b5b6 100644 --- a/tests/lean/macro1.lean.expected.out +++ b/tests/lean/macro1.lean.expected.out @@ -1,7 +1,3 @@ -macro1.lean:8:4: warning: failed to generate bytecode for 'lambda_macro' -code generation failed, VM does not have code for '_unreachable_' -macro1.lean:23:4: warning: failed to generate bytecode for 'ref_macro' -code generation failed, VM does not have code for '_unreachable_' (0: node lambda (1: ident x) (2: node ref (3: ident x))) ((0: node lambda (1: ident x) (2: node ref (3: ident x))), ⟨3 ← ((inl 1), x)⟩) (0: node lambda (1: ident x) (5: node lambda (6: ident x from 0) (2: node ref (3: ident x))))