refactor(library/data/option): move 'option' declaration to init.datatypes

2014-12-03 18:53:23 -08:00 · 2014-12-03 18:53:23 -08:00 · af978e40e8
commit af978e40e8
parent 0f854f592c
2 changed files with 4 additions and 4 deletions
--- 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
--- 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