blob: c9e3292b481c0de5a651022b04b6fff792704018 (
plain)
1
2
3
4
5
6
7
8
|
Goal Type.
let c := constr:(prod nat nat) in
let c' := (eval pattern nat in c) in
let c' := lazymatch c' with ?f _ => f end in
let c'' := lazymatch c' with fun x : Set => ?f => constr:(forall x : Type, f) end in
let _ := type of c'' in
exact c''.
Defined.
|
