diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index da70bc8f5..10258b359 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -653,12 +653,12 @@ static unsigned get_some_precedence(token_table const & t, name const & tk) {
 }
 
 auto pretty_fn::pp_notation_child(expr const & e, unsigned lbp, unsigned rbp) -> result {
-    if (is_app(e) && !m_coercion && is_coercion(m_env, get_app_fn(e))) {
+    if (is_app(e) && is_implicit(app_fn(e))) {
+        return pp_notation_child(app_fn(e), lbp, rbp);
+    } else if (is_app(e) && !m_coercion && is_coercion(m_env, get_app_fn(e))) {
         return pp_coercion(e, rbp);
     } else {
         result r = pp(e);
-        // std::cout << "e:   " << e << "\n";
-        // std::cout << "lbp: " << lbp << ", rbp: " << rbp << ", r.lbp(): " << r.lbp() << ", r.rbp(): " << r.rbp() << "\n\n";
         if (r.rbp() < lbp || r.lbp() <= rbp) {
             return result(paren(r.fmt()));
         } else {
diff --git a/tests/lean/notation2.lean b/tests/lean/notation2.lean
new file mode 100644
index 000000000..9ae820ffe
--- /dev/null
+++ b/tests/lean/notation2.lean
@@ -0,0 +1,5 @@
+import data.list data.num
+open list
+
+check 1 :: 2 :: nil
+check 1 :: 2 :: 3 :: 4 :: 5 :: nil
diff --git a/tests/lean/notation2.lean.expected.out b/tests/lean/notation2.lean.expected.out
new file mode 100644
index 000000000..87bbe382a
--- /dev/null
+++ b/tests/lean/notation2.lean.expected.out
@@ -0,0 +1,3 @@
+notation2.lean:2:0: warning: imported file uses 'sorry'
+1 :: 2 :: nil : list num
+1 :: 2 :: 3 :: 4 :: 5 :: nil : list num