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

feat(library/compiler/util): do not consider constructors to be cost zero

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-26 08:48:06 -07:00
parent 7fed0b5cb0
commit 21b8199bc4
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/util.cpp
View file

@ -363,8 +363,6 @@ unsigned get_lcnf_size(environment const & env, expr e) {
e = app_fn(e);
}
return r;
} else if (is_constructor_app(env, e)) {
return 0;
} else {
return 1;
}