From 4e49e73585e616b7f8899ff64169354bc37ee1bc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 7 Jan 2015 18:45:58 -0800
Subject: [PATCH] refactor(library/init/logic): add inhabited related
 functions, rename inhabited.default to default

---
 library/init/logic.lean           | 7 +++++--
 tests/lean/run/private_names.lean | 2 +-
 2 files changed, 6 insertions(+), 3 deletions(-)

diff --git a/library/init/logic.lean b/library/init/logic.lean
index 742f71cab3..556c9a1114 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -325,10 +325,13 @@ definition decidable_eq   (A : Type) := decidable_rel (@eq A)
 inductive inhabited [class] (A : Type) : Type :=
 mk : A → inhabited A
 
+protected definition inhabited.value {A : Type} (h : inhabited A) : A :=
+inhabited.rec (λa, a) h
+
 protected definition inhabited.destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B :=
 inhabited.rec H2 H1
 
-definition inhabited.default (A : Type) [H : inhabited A] : A :=
+definition default (A : Type) [H : inhabited A] : A :=
 inhabited.rec (λa, a) H
 
 opaque definition arbitrary (A : Type) [H : inhabited A] : A :=
@@ -351,7 +354,7 @@ protected definition nonempty.elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 :
 nonempty.rec H2 H1
 
 theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A :=
-nonempty.intro (inhabited.default A)
+nonempty.intro (default A)
 
 definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A :=
 decidable.rec_on H (λ Hc, t) (λ Hnc, e)
diff --git a/tests/lean/run/private_names.lean b/tests/lean/run/private_names.lean
index c6b013bd91..c194ab6f84 100644
--- a/tests/lean/run/private_names.lean
+++ b/tests/lean/run/private_names.lean
@@ -5,7 +5,7 @@ section
 
   instance [priority 1000] foo
 
-  example : inhabited.default Prop = false :=
+  example : default Prop = false :=
   rfl
 end
 end bla