From af978e40e8f3abf419cd61d67d5bb1c2a7a0edcc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Dec 2014 18:53:23 -0800
Subject: [PATCH] refactor(library/data/option): move 'option' declaration to
 init.datatypes

---
 library/data/option.lean    | 4 ----
 library/init/datatypes.lean | 4 ++++
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/library/data/option.lean b/library/data/option.lean
index c2e3c1b324..ad8bcf0eed 100644
--- a/library/data/option.lean
+++ b/library/data/option.lean
@@ -4,10 +4,6 @@
 import logic.eq
 open eq.ops decidable
 
-inductive option (A : Type) : Type :=
-  none {} : option A,
-  some    : A → option A
-
 namespace option
   definition is_none {A : Type} (o : option A) : Prop :=
   rec true (λ a, false) o
diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean
index 8d50342f67..8dda9cca0e 100644
--- a/library/init/datatypes.lean
+++ b/library/init/datatypes.lean
@@ -76,3 +76,7 @@ str   : char → string → string
 inductive nat :=
 zero : nat,
 succ : nat → nat
+
+inductive option (A : Type) : Type :=
+none {} : option A,
+some    : A → option A