michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/abbreviation): apply eta-reduction when expanding abbreviations

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-10 13:40:00 -07:00
parent cff7b7474a
commit 46d418af3d
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/abbreviation.cpp
View file

@ -112,7 +112,7 @@ expr expand_abbreviations(environment const & env, expr const & e) {
abbrev_state const & s = abbrev_ext::get_state(env);
return replace(e, [&](expr const & e, unsigned) {
if (is_constant(e) && s.is_abbreviation(const_name(e)))
return some_expr(instantiate_value_univ_params(env.get(const_name(e)), const_levels(e)));
return some_expr(try_eta(instantiate_value_univ_params(env.get(const_name(e)), const_levels(e))));
else
return none_expr();
});