diff --git a/library/init/list.lean b/library/init/list.lean
index 5d401fe5df..73ace3e8a6 100644
--- a/library/init/list.lean
+++ b/library/init/list.lean
@@ -25,10 +25,11 @@ list.rec_on l₁
              (λ Hne : l₁ ≠ l₂, ff (λ H, list.no_confusion H (λ Hab Hl₁l₂, absurd Hl₁l₂ Hne)))
              (λ He  : l₁ = l₂, tt (congr (congr_arg cons Hab) He)))))
 
-namespace list
 notation h :: t  := cons h t
 notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l
 
+namespace list
+
 variable {A : Type}
 
 definition append : list A → list A → list A