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

fix(frontends/lean/pp): make sure pp doesn't group [] arguments

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-13 12:23:22 -08:00
parent a9b567296c
commit 9a4a12899a
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/frontends/lean/pp.cpp
View file

@ -693,7 +693,7 @@ format pretty_fn::pp_binders(buffer<expr> const & locals) {
format r;
for (unsigned i = 1; i < num; i++) {
expr local = locals[i];
if (mlocal_type(local) == type && local_info(local) == bi) {
if (!bi.is_inst_implicit() && mlocal_type(local) == type && local_info(local) == bi) {
names.push_back(local_pp_name(local));
} else {
r += group(compose(line(), pp_binder_block(names, type, bi)));