From 8adf6e25ef3f88fb3e8c600c8da9b1b48b6a488a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Jul 2014 09:56:05 -0700 Subject: [PATCH] refactor(library/standard/unit): make unit type similar to the one in the hott library Signed-off-by: Leonardo de Moura --- library/standard/unit.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/library/standard/unit.lean b/library/standard/unit.lean index 4bdefb1b6..46ecfc63f 100644 --- a/library/standard/unit.lean +++ b/library/standard/unit.lean @@ -6,13 +6,15 @@ using decidable namespace unit inductive unit : Type := -| tt : unit +| star : unit + +notation `⋆`:max := star theorem unit_eq (a b : unit) : a = b -:= unit_rec (unit_rec (refl tt) b) a +:= unit_rec (unit_rec (refl ⋆) b) a theorem inhabited_unit [instance] : inhabited unit -:= inhabited_intro tt +:= inhabited_intro ⋆ using decidable theorem decidable_eq [instance] (a b : unit) : decidable (a = b)