blob: 4164d86dc18bc3aa781759109c484f51c846fabe (
plain)
1
2
3
4
5
6
|
Definition id {T} (x : T) := x.
Goal sigT (fun x => id x)%type.
change (fun x => ?f x) with f.
Unshelve.
exists Type. exact Set.
Defined. (* Error: Attempt to save a proof with shelved goals (in proof Unnamed_thm) *)
|
