refactor(library/data): remove folders with a single file

library/data/bool.lean

@@ -2,7 +2,7 @@
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Module: data.bool.thms
+Module: data.bool
 Author: Leonardo de Moura
 -/
 

library/data/bool/default.lean

@@ -1,9 +0,0 @@
-/-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.bool.default
-Author: Leonardo de Moura
--/
-
-import data.bool.thms

library/data/data.md

@@ -7,8 +7,8 @@ Basic types:
 
 * [empty](empty.lean) : the empty type
 * [unit](unit.lean) : the singleton type
-* [bool](bool/bool.md) : the boolean values
+* [bool](bool.lean) : the boolean values
-* [num](num/num.md) : generic numerals
+* [num](num.lean) : generic numerals
 * [string](string.lean) : ascii strings
 * [nat](nat/nat.md) : the natural numbers
 * [fin](fin.lean) : finite ordinals

library/data/empty.lean

@@ -1,9 +1,11 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+/-
--- Released under Apache 2.0 license as described in the file LICENSE.
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Author: Jeremy Avigad, Floris van Doorn
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.empty
+Author: Jeremy Avigad, Floris van Doorn
+-/
 
--- Empty type
--- ----------
 import logic.cast logic.subsingleton
 
 namespace empty

library/data/num.lean

@@ -2,7 +2,7 @@
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Module: data.num.thms
+Module: data.num
 Author: Leonardo de Moura
 -/
 

library/data/num/default.lean

@@ -1,9 +0,0 @@
-/-
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.num.default
-Author: Leonardo de Moura
--/
-
-import data.num.thms

library/data/prod.lean

@@ -1,6 +1,11 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+/-
--- Released under Apache 2.0 license as described in the file LICENSE.
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Author: Leonardo de Moura, Jeremy Avigad
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.prod
+Author: Leonardo de Moura, Jeremy Avigad
+-/
+
 import logic.eq
 open inhabited decidable eq.ops
 

library/data/prod/default.lean

@@ -1,4 +0,0 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura, Jeremy Avigad
-import data.prod.thms

library/data/sigma/default.lean

@@ -1,4 +0,0 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
-import data.sigma.thms

library/data/string.lean

@@ -1,6 +1,11 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+/-
--- Released under Apache 2.0 license as described in the file LICENSE.
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Author: Leonardo de Moura
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.string
+Author: Leonardo de Moura
+-/
+
 import data.bool
 open bool inhabited
 

library/data/string/default.lean

@@ -1,4 +0,0 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura
-import data.string.thms

library/data/unit.lean

@@ -0,0 +1,28 @@
+/-
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Module: data.unit
+Author: Leonardo de Moura
+-/
+
+import logic.eq logic.subsingleton
+
+namespace unit
+  notation `⋆` := star
+
+  protected theorem equal (a b : unit) : a = b :=
+  rec_on a (rec_on b rfl)
+
+  theorem eq_star (a : unit) : a = star :=
+  equal a star
+
+  protected theorem subsingleton [instance] : subsingleton unit :=
+  subsingleton.intro (λ a b, equal a b)
+
+  protected definition is_inhabited [instance] : inhabited unit :=
+  inhabited.mk unit.star
+
+  protected definition has_decidable_eq [instance] : decidable_eq unit :=
+  take (a b : unit), decidable.inl (equal a b)
+end unit

library/data/unit/default.lean

@@ -1,7 +0,0 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura
-import data.unit.thms data.unit.insts
-namespace unit
-  notation `⋆` := star
-end unit

library/data/unit/insts.lean

@@ -1,16 +0,0 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura
-import data.unit.thms logic.subsingleton
-open decidable
-
-namespace unit
-  protected theorem subsingleton [instance] : subsingleton unit :=
-  subsingleton.intro (λ a b, equal a b)
-
-  protected definition is_inhabited [instance] : inhabited unit :=
-  inhabited.mk unit.star
-
-  protected definition has_decidable_eq [instance] : decidable_eq unit :=
-  take (a b : unit), inl (equal a b)
-end unit

library/data/unit/thms.lean

@@ -1,12 +0,0 @@
--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
--- Released under Apache 2.0 license as described in the file LICENSE.
--- Author: Leonardo de Moura
-import logic.eq
-
-namespace unit
-  protected theorem equal (a b : unit) : a = b :=
-  rec_on a (rec_on b rfl)
-
-  theorem eq_star (a : unit) : a = star :=
-  equal a star
-end unit