From 354b50a1f56389f86b222763f80affb66e593ee8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 25 Oct 2014 13:55:03 -0700
Subject: [PATCH] refactor(library/data/unit): make unit universe polymorphic

Motivation: we need it for "padding".
Example 1: defining a n-ary tuple type.
Example 2: defining cases-on for mutually recursive datatypes
---
 library/data/unit.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/data/unit.lean b/library/data/unit.lean
index fad608890..0694735df 100644
--- a/library/data/unit.lean
+++ b/library/data/unit.lean
@@ -4,14 +4,14 @@
 import logic.decidable logic.inhabited
 open decidable
 
-inductive unit : Type :=
+inductive unit.{l} : Type.{l} :=
   star : unit
 namespace unit
   notation `⋆` := star
 
   -- remove duplication?
   protected theorem equal (a b : unit) : a = b :=
-  rec (rec rfl b) a
+  rec_on a (rec_on b rfl)
 
   protected theorem subsingleton [instance] : subsingleton unit :=
   subsingleton.intro (λ a b, equal a b)