blob: f5ce981cd069958f3dd4ae2b84ae8295cd78203c (
plain)
1
2
3
4
5
6
7
|
Record foo := mkfoo { type : Type }.
Canonical Structure fooA (T : Type) := mkfoo (T -> T).
Definition id (t : foo) (x : type t) := x.
Definition bar := id _ ((fun x : nat => x) : _).
|