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

fix(library/compiler/struct_cases_on): bug and missing case

Browse source
This commit is contained in:
Leonardo de Moura 2019-05-03 20:03:03 -07:00
parent 6f971382be
commit 04670c4127
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/struct_cases_on.cpp
View file

@ -154,7 +154,7 @@ class struct_cases_on_fn {
while (is_let(e)) {
lean_assert(!has_loose_bvars(let_type(e)));
expr type = let_type(e);
expr val = instantiate_rev(let_value(e), fvars.size(), fvars.data());
expr val = visit(instantiate_rev(let_value(e), fvars.size(), fvars.data()));
name n = let_name(e);
e = let_body(e);
expr new_fvar = m_lctx.mk_local_decl(ngen(), n, type, val);
@ -177,7 +177,7 @@ class struct_cases_on_fn {
e = mk_let(decl.get_user_name(), type, aval, e);
if (should_add_cases_on(decl)) {
lean_assert(is_proj(val));
expr major = proj_expr(val);
expr major = proj_expr(aval);
buffer<expr> field_types;
get_struct_field_types(m_st, proj_sname(val), field_types);
e = lift_loose_bvars(e, field_types.size());