blob: d41d231739450a18a24cc3c433216ac7cfce8c86 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Set Implicit Arguments.
Ltac ret_and_left T :=
let t := type of T in
lazymatch eval hnf in t with
| ?a /\ ?b => constr:(proj1 T)
| forall x : ?T', @?f x =>
constr:(fun x : T' => $(let fx := constr:(T x) in
let t := ret_and_left fx in
exact t)$)
end.
|
