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