diff options
| -rw-r--r-- | theories/Init/Datatypes.v | 10 |
1 files changed, 8 insertions, 2 deletions
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), |