blob: 9c85839b7503438f3cbd6015aeae626341cefdfa (
plain)
1
2
3
4
5
6
7
8
|
Record foo : Type :=
{ fooA : Type; fooB : Type }.
Definition id {A : Type} (a : A) := a.
Definition untypable : Type.
unshelve refine (let X := _ in let Y : _ := ltac:(let ty := type of X in exact ty) in id Y).
exact foo.
constructor. exact unit. exact unit.
Defined.
|
