From 758a17ab23bc992bffff94dbe93c50269db60694 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 25 Oct 2014 14:57:33 -0700
Subject: [PATCH] refactor(library/data/unit): break unit.lean into smaller
 pieces

The unit datatype is used by automation.

We want to be able to access its declaration without having to access
all dependencies (e.g., decidable, subsingleton, inhabited, ...).

This is *not* an optimization, but a way to make sure we can "import" unit
before we import other declarations.
---
 library/data/unit/basic.lean                |  5 +++++
 library/data/unit/decl.lean                 |  9 +++++++++
 library/data/unit/default.lean              |  4 ++++
 library/data/{unit.lean => unit/insts.lean} | 13 +------------
 4 files changed, 19 insertions(+), 12 deletions(-)
 create mode 100644 library/data/unit/basic.lean
 create mode 100644 library/data/unit/decl.lean
 create mode 100644 library/data/unit/default.lean
 rename library/data/{unit.lean => unit/insts.lean} (65%)

diff --git a/library/data/unit/basic.lean b/library/data/unit/basic.lean
new file mode 100644
index 000000000..df303f48e
--- /dev/null
+++ b/library/data/unit/basic.lean
@@ -0,0 +1,5 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+inductive unit.{l} : Type.{l} :=
+  star : unit
diff --git a/library/data/unit/decl.lean b/library/data/unit/decl.lean
new file mode 100644
index 000000000..2860fbec1
--- /dev/null
+++ b/library/data/unit/decl.lean
@@ -0,0 +1,9 @@
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Leonardo de Moura
+inductive unit.{l} : Type.{l} :=
+  star : unit
+
+namespace unit
+  notation `⋆` := star
+end unit
diff --git a/library/data/unit/default.lean b/library/data/unit/default.lean
new file mode 100644
index 000000000..7b2dbca50
--- /dev/null
+++ b/library/data/unit/default.lean
@@ -0,0 +1,4 @@
+-- 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.decl data.unit.thms data.unit.insts
diff --git a/library/data/unit.lean b/library/data/unit/insts.lean
similarity index 65%
rename from library/data/unit.lean
rename to library/data/unit/insts.lean
index 0694735df..6f7cf442e 100644
--- a/library/data/unit.lean
+++ b/library/data/unit/insts.lean
@@ -1,24 +1,13 @@
 -- 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.decidable logic.inhabited
+import data.unit.decl data.unit.thms logic.decidable logic.inhabited
 open decidable
 
-inductive unit.{l} : Type.{l} :=
-  star : unit
 namespace unit
-  notation `⋆` := star
-
-  -- remove duplication?
-  protected theorem equal (a b : unit) : a = b :=
-  rec_on a (rec_on b rfl)
-
   protected theorem subsingleton [instance] : subsingleton unit :=
   subsingleton.intro (λ a b, equal a b)
 
-  theorem eq_star (a : unit) : a = star :=
-  equal a star
-
   protected definition is_inhabited [instance] : inhabited unit :=
   inhabited.mk ⋆