From e2abb4ab2547a854abcd9df71d7a73cd75913ba1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Apr 2018 08:50:56 -0700
Subject: [PATCH] chore(library/init): remove `punit` micro module

---
 library/init/core.lean       | 21 +++++++++++++++++++--
 library/init/data/basic.lean |  3 +--
 library/init/data/punit.lean | 22 ----------------------
 3 files changed, 20 insertions(+), 26 deletions(-)
 delete mode 100644 library/init/data/punit.lean

diff --git a/library/init/core.lean b/library/init/core.lean
index 75896f6a5e..823d2047fd 100644
--- a/library/init/core.lean
+++ b/library/init/core.lean
@@ -1633,7 +1633,7 @@ end subtype
 section
 variables {α : Type u} {β : Type v}
 
-@[simp] lemma prod.mk.eta : ∀{p : α × β}, (p.1, p.2) = p
+@[simp] theorem prod.mk.eta : ∀{p : α × β}, (p.1, p.2) = p
 | (a, b) := rfl
 
 instance [inhabited α] [inhabited β] : inhabited (prod α β) :=
@@ -1660,10 +1660,27 @@ instance prod_has_decidable_lt
          [decidable_rel ((<) : β → β → Prop)] : Π s t : α × β, decidable (s < t) :=
 λ t s, or.decidable
 
-lemma prod.lt_def [has_lt α] [has_lt β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
+theorem prod.lt_def [has_lt α] [has_lt β] (s t : α × β) : (s < t) = (s.1 < t.1 ∨ (s.1 = t.1 ∧ s.2 < t.2)) :=
 rfl
 end
 
 def {u₁ u₂ v₁ v₂} prod.map {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
   (f : α₁ → α₂) (g : β₁ → β₂) : α₁ × β₁ → α₂ × β₂
 | (a, b) := (f a, g b)
+
+/- Universe polymorphic unit -/
+
+theorem punit_eq (a b : punit) : a = b :=
+punit.rec_on a (punit.rec_on b rfl)
+
+theorem punit_eq_punit (a : punit) : a = () :=
+punit_eq a ()
+
+instance : subsingleton punit :=
+subsingleton.intro punit_eq
+
+instance : inhabited punit :=
+⟨()⟩
+
+instance : decidable_eq punit :=
+λ a b, is_true (punit_eq a b)
diff --git a/library/init/data/basic.lean b/library/init/data/basic.lean
index 6c4f4f9804..4a6f9d4c84 100644
--- a/library/init/data/basic.lean
+++ b/library/init/data/basic.lean
@@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.setoid init.data.quot init.data.punit
-import init.data.nat.basic init.data.sum.basic
+import init.data.setoid init.data.quot init.data.nat.basic init.data.sum.basic
 import init.data.sigma.basic init.data.fin.basic init.data.list.basic init.data.char.basic
 import init.data.string.basic init.data.option.basic init.data.set
 import init.data.uint init.data.ordering.basic init.data.repr
diff --git a/library/init/data/punit.lean b/library/init/data/punit.lean
deleted file mode 100644
index c1be8c0b90..0000000000
--- a/library/init/data/punit.lean
+++ /dev/null
@@ -1,22 +0,0 @@
-/-
-Copyright (c) 2016 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Author: Leonardo de Moura
--/
-prelude
-import init.core
-
-lemma punit_eq (a b : punit) : a = b :=
-punit.rec_on a (punit.rec_on b rfl)
-
-lemma punit_eq_punit (a : punit) : a = () :=
-punit_eq a ()
-
-instance : subsingleton punit :=
-subsingleton.intro punit_eq
-
-instance : inhabited punit :=
-⟨()⟩
-
-instance : decidable_eq punit :=
-λ a b, is_true (punit_eq a b)