blob: 2e81a183cde4b3fc85541341a8c85de852b3ce6a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
(* Original example *)
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
exact c''.
Fail Defined.
Abort.
(* Workaround *)
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.
|
