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

chore(library/compiler/csimp): compilation error in debug mode

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-17 07:40:47 -07:00
parent 32a309c566
commit f12e580ac2
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/csimp.cpp
View file

@ -1154,7 +1154,7 @@ class csimp_fn {
return some_expr(s);
} else if (is_proj(s)) {
if (optional<expr> new_nested_s = try_inline_proj_instance_aux(proj_expr(s))) {
lean_assert(is_constructor_app(env(), new_nested_s));
lean_assert(is_constructor_app(env(), *new_nested_s));
expr r = proj_constructor(*new_nested_s, proj_idx(s).get_small_value());
return try_inline_proj_instance_aux(r);
}
@ -1216,7 +1216,7 @@ class csimp_fn {
unsigned saved_fvars_size = m_fvars.size();
if (optional<expr> new_s = try_inline_proj_instance_aux(proj_expr(e))) {
lean_assert(is_constructor_app(env(), new_s));
lean_assert(is_constructor_app(env(), *new_s));
expr r = proj_constructor(*new_s, proj_idx(e).get_small_value());
return some_expr(visit(r, is_let_val));
}