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

fix(frontends/lean/pp): abbreviations with too much arguments

Browse source 
closes #480
This commit is contained in:
Leonardo de Moura 2015-03-23 12:16:25 -07:00
parent 0814e76298
commit 76157ba392
3 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/pp.cpp
View file

@ -1073,10 +1073,10 @@ auto pretty_fn::pp_abbreviation(expr const & e, name const & abbrev, bool fn, un
buffer<level> ls; buffer<level> ls;
for (unsigned i = 0; i < num_univs; i++) for (unsigned i = 0; i < num_univs; i++)
ls.push_back(mk_meta_univ(name("?l", i+1))); ls.push_back(mk_meta_univ(name("?l", i+1)));
buffer<expr> args; expr r = mk_constant(abbrev, to_list(ls));
if (fn) if (fn)
get_app_args(e, args); r = mk_app(r, app_arg(e));
return pp_child(mk_app(mk_constant(abbrev, to_list(ls)), args), bp, ignore_hide); return pp_child(r, bp, ignore_hide);
} }
static bool is_pp_atomic(expr const & e) { static bool is_pp_atomic(expr const & e) {

2
tests/lean/480.hlean Normal file
View file

@ -0,0 +1,2 @@
open is_trunc
check is_contr.mk

1
tests/lean/480.hlean.expected.out Normal file
View file

@ -0,0 +1 @@
is_contr.mk : Π (center : ?A), (Π (a : ?A), center = a) → is_contr ?A