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

fix(library/compiler/vm_compiler): add support for kernel projections

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-29 17:13:55 -07:00
parent 86d5ccf8f5
commit cdc0a5ac29
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -283,8 +283,9 @@ class vm_compiler_fn {
}
}
void compile_proj_cnstr(expr const & /* e */, unsigned /* bpz */, name_map<unsigned> const & /* m */) {
lean_unreachable();
void compile_proj_cnstr(expr const & e, unsigned bpz, name_map<unsigned> const & m) {
compile(proj_expr(e), bpz, m);
emit(mk_proj_instr(proj_idx(e).get_small_value()));
}
void compile(expr const & e, unsigned bpz, name_map<unsigned> const & m) {