diff options
| -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 *) |