diff options
| author | Yishuai Li | 2020-07-20 21:59:37 -0400 |
|---|---|---|
| committer | Yishuai Li | 2020-08-11 18:52:07 -0400 |
| commit | c34596ab97743ddc3761f72f61edfd856bd2804e (patch) | |
| tree | 7995a47bc31bd98a78d3dc00007ae6207ef46d15 | |
| parent | e0e07f58da0d45ab54558c61a4a1c3074dfb6380 (diff) | |
deprecate prod_curry and prod_uncurry
| -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), |