From 7e15b114e6517bdac9bf2c09234eebe18dce06e9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Jun 2016 18:15:43 -0700
Subject: [PATCH] refactor(library/init/list): move list notation to the
 top-level

---
 library/init/list.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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