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

fix(library/init/logic): expose inhabited basic instances

Browse source
This commit is contained in:
Leonardo de Moura 2014-12-13 14:26:44 -08:00
parent c291063f3a
commit 6e84696960
1 changed files with 11 additions and 16 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
library/init/logic.lean
View file

@ -327,35 +327,30 @@ definition decidable_eq (A : Type) := decidable_rel (@eq A)
inductive inhabited [class] (A : Type) : Type := inductive inhabited [class] (A : Type) : Type :=
mk : A → inhabited A mk : A → inhabited A
namespace inhabited protected definition inhabited.destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B :=
protected definition destruct {A : Type} {B : Type} (H1 : inhabited A) (H2 : A → B) : B :=
inhabited.rec H2 H1 inhabited.rec H2 H1
definition inhabited.default (A : Type) [H : inhabited A] : A :=
inhabited.rec (λa, a) H
definition Prop_inhabited [instance] : inhabited Prop := definition Prop_inhabited [instance] : inhabited Prop :=
mk true inhabited.mk true
definition fun_inhabited [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) := definition fun_inhabited [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) :=
destruct H (λb, mk (λa, b)) inhabited.rec_on H (λb, inhabited.mk (λa, b))
definition dfun_inhabited [instance] (A : Type) {B : A → Type} (H : Πx, inhabited (B x)) : definition dfun_inhabited [instance] (A : Type) {B : A → Type} (H : Πx, inhabited (B x)) :
inhabited (Πx, B x) := inhabited (Πx, B x) :=
mk (λa, destruct (H a) (λb, b)) inhabited.mk (λa, inhabited.rec_on (H a) (λb, b))
definition default (A : Type) [H : inhabited A] : A := destruct H (take a, a)
end inhabited
inductive nonempty [class] (A : Type) : Prop := inductive nonempty [class] (A : Type) : Prop :=
intro : A → nonempty A intro : A → nonempty A
namespace nonempty protected definition nonempty.elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B :=
protected definition elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B := nonempty.rec H2 H1
rec H2 H1
theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A := theorem inhabited_imp_nonempty [instance] {A : Type} (H : inhabited A) : nonempty A :=
intro (inhabited.default A) nonempty.intro (inhabited.default A)
end nonempty
definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A := definition ite (c : Prop) [H : decidable c] {A : Type} (t e : A) : A :=
decidable.rec_on H (λ Hc, t) (λ Hnc, e) decidable.rec_on H (λ Hc, t) (λ Hnc, e)