6 lines
110 B
Text
6 lines
110 B
Text
section
|
|
parameter A : Type
|
|
definition tst (a : A) := a
|
|
set_option pp.universes true
|
|
check tst.{1}
|
|
end
|