16 lines
224 B
Text
16 lines
224 B
Text
|
variables (A : Type) [inhabited A]
|
||
|
|
|
||
|
|
definition f (a : A) : A := a
|
||
|
|
|
||
|
|
check @f nat nat.is_inhabited
|
||
|
|
|
||
|
|
structure foo :=
|
||
|
|
(a : A)
|
||
|
|
|
||
|
|
check @foo nat nat.is_inhabited
|
||
|
|
|
||
|
|
inductive bla :=
|
||
|
|
| mk : A → bla
|
||
|
|
|
||
|
|
check @bla nat nat.is_inhabited
|