From b0abea78b6b40fa620c79c752a04aba70401ea4b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 16 Aug 2016 10:34:04 -0700
Subject: [PATCH] fix(frontends/lean/pp): bug when pretty printing foldr/foldl
 notation

---
 src/frontends/lean/pp.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 9d0fe1b326..152a17019b 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -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))