michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/standard/unit): make unit type similar to the one in the hott library

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-22 09:56:05 -07:00
parent c5cbe1cc2c
commit 8adf6e25ef
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
library/standard/unit.lean
View file

@ -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)