From 840ef98829b847851d70105c8f58f1127c6c0ee7 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Thu, 27 Aug 2015 13:46:00 -0400
Subject: [PATCH] refactor(library/init/nat): make \nat notation available at
 top level

---
 library/data/int/div.lean | 1 -
 library/init/nat.lean     | 3 ++-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index d23eef584..add7a9679 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -11,7 +11,6 @@ import data.int.order data.nat.div
 open [coercions] [reduce-hints] nat
 open [declarations] nat (succ)
 open eq.ops
-notation `ℕ` := nat
 
 namespace int
 
diff --git a/library/init/nat.lean b/library/init/nat.lean
index 18e4f1dbc..8ac028be3 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -7,8 +7,9 @@ prelude
 import init.wf init.tactic init.num
 open eq.ops decidable or
 
+notation `ℕ` := nat
+
 namespace nat
-  notation `ℕ` := nat
 
   /- basic definitions on natural numbers -/
   inductive le (a : ℕ) : ℕ → Prop :=