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

fix(frontends/lean/pp): bug when pretty printing foldr/foldl notation

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-16 10:34:04 -07:00
parent 100a15cb0d
commit b0abea78b6
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

@ -1367,7 +1367,7 @@ auto pretty_fn::pp_notation(notation_entry const & entry, buffer<optional<expr>>
e = *new_e;
matched_once = true;
}
if (!matched_once)
if (!matched_once && ini)
return optional<result>();
if (ini) {
if (!match(*ini, e, args))