blob: 410fe1707d7530a43186f0ba43aef3ce9097d34a (
plain)
1
2
3
4
5
6
|
Set Universe Polymorphism.
Record cantype := {T:Type; op:T -> unit}.
Canonical Structure test (P:Type) := {| T := P -> Type; op := fun _ => tt|}.
Check (op _ ((fun (_:unit) => Set):_)).
|