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

refactor(library/init/logic): add inhabited related functions, rename inhabited.default to default

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-07 18:45:58 -08:00
parent 1fab144aa7
commit 4e49e73585
2 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/init/logic.lean
View file

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

2
tests/lean/run/private_names.lean
View file

@ -5,7 +5,7 @@ section
instance [priority 1000] foo
example : inhabited.default Prop = false :=
example : default Prop = false :=
rfl
end
end bla