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

fix(library/composition_manager): typo

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-27 14:12:26 -07:00
parent ca0aa4eb47
commit 8616ed096e
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/composition_manager.cpp
View file

@ -115,7 +115,7 @@ pair<environment, name> compose(environment const & env, type_checker & tc, name
} else { } else {
// do not expand // do not expand
expr b = mk_app(mk_constant(f, f_ls), f_domain); expr b = mk_app(mk_constant(f, f_ls), f_domain);
new_val_body = Fun(f_domain, mk_app(mk_app(mk_constant(g, const_levels(B)), B_args), b)); new_val_body = mk_app(mk_app(mk_constant(g, const_levels(B)), B_args), b);
} }
expr new_val = Fun(f_domain, new_val_body); expr new_val = Fun(f_domain, new_val_body);
expr new_type; expr new_type;