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

fix(library/init/logic.lean): rename inhabited_imp_nonempty

Browse source
This commit is contained in:
Jeremy Avigad 2015-03-25 17:40:55 -04:00 committed by Leonardo de Moura
parent 8e007b3441
commit e019ab5500
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/logic.lean
View file

@ -365,7 +365,7 @@ intro : A → nonempty A
protected definition nonempty.elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B := protected definition nonempty.elim {A : Type} {B : Prop} (H1 : nonempty A) (H2 : A → B) : B :=
nonempty.rec H2 H1 nonempty.rec H2 H1
theorem inhabited_imp_nonempty [instance] {A : Type} [H : inhabited A] : nonempty A := theorem nonempty_of_inhabited [instance] {A : Type} [H : inhabited A] : nonempty A :=
nonempty.intro (default A) nonempty.intro (default A)
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 :=