diff options
| author | Anton Trunov | 2020-08-13 18:27:34 +0300 |
|---|---|---|
| committer | Anton Trunov | 2020-08-13 18:27:34 +0300 |
| commit | 226ed2069d9874fe845a1995053783f811ace9ae (patch) | |
| tree | 364c569bbce80a00482758109a4548eb7daa782c | |
| parent | ae5f5ba7f7e673dfeb06a9feaa4271fc165d01f3 (diff) | |
| parent | 5169633a26d2639ec43b4ec82dff11348e380825 (diff) | |
Merge PR #12716: deprecate prod_curry and prod_uncurry
Reviewed-by: anton-trunov
| -rw-r--r-- | doc/changelog/10-standard-library/12716-curry.rst | 4 | ||||
| -rw-r--r-- | theories/Init/Datatypes.v | 10 |
2 files changed, 12 insertions, 2 deletions
diff --git a/doc/changelog/10-standard-library/12716-curry.rst b/doc/changelog/10-standard-library/12716-curry.rst new file mode 100644 index 0000000000..51b59e4a94 --- /dev/null +++ b/doc/changelog/10-standard-library/12716-curry.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + ``prod_curry`` and ``prod_uncurry``, in favor of ``uncurry`` and ``curry`` + (`#12716 <https://github.com/coq/coq/pull/12716>`_, + by Yishuai Li). diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 8ab12ae534..77be679070 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -272,12 +272,18 @@ Proof with auto. - destruct H; subst... Qed. -Definition prod_uncurry (A B C:Type) (f:A * B -> C) +Definition curry {A B C:Type} (f:A * B -> C) (x:A) (y:B) : C := f (x,y). -Definition prod_curry (A B C:Type) (f:A -> B -> C) +Definition uncurry {A B C:Type} (f:A -> B -> C) (p:A * B) : C := match p with (x, y) => f x y end. +#[deprecated(since = "8.13", note = "Use curry instead.")] +Definition prod_uncurry (A B C:Type) : (A * B -> C) -> A -> B -> C := curry. + +#[deprecated(since = "8.13", note = "Use uncurry instead.")] +Definition prod_curry (A B C:Type) : (A -> B -> C) -> A * B -> C := uncurry. + Import EqNotations. Lemma rew_pair : forall A (P Q : A->Type) x1 x2 (y1:P x1) (y2:Q x1) (H:x1=x2), |