2014-10-08 15:37:54 +00:00
|
|
|
import logic
|
|
|
|
|
|
|
|
|
|
|
2014-10-12 20:06:00 +00:00
|
|
|
definition foo {A : Type} [H : inhabited A] : A :=
|
2014-10-08 15:37:54 +00:00
|
|
|
inhabited.rec (λa, a) H
|
|
|
|
|
|
2014-10-12 20:06:00 +00:00
|
|
|
constant bla {A : Type} [H : inhabited A] : Type.{1}
|
2014-10-08 15:37:54 +00:00
|
|
|
|
|
|
|
|
set_option pp.implicit true
|
|
|
|
|
|
|
|
|
|
section
|
|
|
|
|
variable A : Type
|
|
|
|
|
variable S : inhabited A
|
|
|
|
|
variable B : bla
|
|
|
|
|
check B
|
|
|
|
|
check @foo A _
|
|
|
|
|
end
|
