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

feat(library/classes/inhabited): add dfun_inhabited theorem

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-07 19:06:42 -07:00
parent 4e2f5572f3
commit 48e5a2b6ad
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/logic/classes/inhabited.lean
View file

@ -16,7 +16,10 @@ definition Prop_inhabited [instance] : inhabited Prop :=
mk true
definition fun_inhabited [instance] (A : Type) {B : Type} (H : inhabited B) : inhabited (A → B) :=
destruct H (take b, mk (λa, b))
destruct H (λb, mk (λa, b))
definition dfun_inhabited [instance] (A : Type) {B : A → Type} (H : Πx, inhabited (B x)) : inhabited (Πx, B x) :=
mk (λa, destruct (H a) (λb, b))
definition default (A : Type) {H : inhabited A} : A := destruct H (take a, a)