diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-10-20 13:35:46 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-10-20 13:35:46 -0400 |
| commit | f32c60ffa460088bd3b9a15976ba3bd347e2e623 (patch) | |
| tree | 2d2c87b8563b3c0e1a0f2bc82487f94d08b3926b /src/Util/Curry.v | |
| parent | 6817b8c6a0bfc23a8b3a26592f91c1566322185c (diff) | |
Add curry{3,4}
Diffstat (limited to 'src/Util/Curry.v')
| -rw-r--r-- | src/Util/Curry.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Util/Curry.v b/src/Util/Curry.v index d1e3a7b94..22747ed23 100644 --- a/src/Util/Curry.v +++ b/src/Util/Curry.v @@ -1,7 +1,11 @@ Require Import Crypto.Util.Tactics.ChangeInAll. Definition curry2 {A B C} (f : A -> B -> C) (x : A * B) : C -:= let '(a, b) := x in f a b. + := let '(a, b) := x in f a b. +Definition curry3 {A B C D} (f : A -> B -> C -> D) (x : A * B * C) : D + := let '(a, b, c) := x in f a b c. +Definition curry4 {A B C D E} (f : A -> B -> C -> D -> E) (x : A * B * C * D) : E + := let '(a, b, c, d) := x in f a b c d. Ltac change_with_curried f := cbv beta in f; (* work around https://coq.inria.fr/bugs/show_bug.cgi?id=5430 *) |