From b094c1cf43afac6f829bf759d3a79e666e0635dc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 1 Dec 2014 08:23:31 -0800
Subject: [PATCH] refactor(library/init): move num->nat coercion to init

---
 library/data/nat/basic.lean | 4 ----
 library/init/nat.lean       | 3 +++
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index 9afb91f72..eea1177ae 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -10,10 +10,6 @@ open eq.ops binary
 
 namespace nat
 
-definition of_num [coercion] [reducible] (n : num) : ℕ :=
-num.rec zero
-  (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
-
 definition addl (x y : ℕ) : ℕ :=
 nat.rec y (λ n r, succ r) x
 infix `⊕`:65 := addl
diff --git a/library/init/nat.lean b/library/init/nat.lean
index a937da29f..291eedbb4 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -338,4 +338,7 @@ namespace nat
     (le.refl a)
     (λ b₁ ih, le.trans !pred_le ih)
 
+  definition of_num [coercion] [reducible] (n : num) : ℕ :=
+  num.rec zero
+    (λ n, pos_num.rec (succ zero) (λ n r, r + r + (succ zero)) (λ n r, r + r) n) n
 end nat