X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fdatatypes%2Fconstructors.ma;h=3f74db5ad85cfb8b7e9ce99d414471fe53f88f3b;hb=7cb659c0af2d665c649f87922be02eccde795542;hp=2ac1cb376804ad8e89dbd2a805cbd9c1c1284065;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/library/datatypes/constructors.ma b/matita/library/datatypes/constructors.ma
index 2ac1cb376..3f74db5ad 100644
--- a/matita/library/datatypes/constructors.ma
+++ b/matita/library/datatypes/constructors.ma
@@ -36,3 +36,14 @@ qed.
 inductive Sum (A,B:Set) : Set \def
   inl : A \to Sum A B
 | inr : B \to Sum A B.
+
+inductive ProdT (A,B:Type) : Type \def
+pairT : A \to B \to ProdT A B.
+
+definition fstT \def \lambda A,B:Type.\lambda p: ProdT A B.
+match p with
+[(pairT a b) \Rightarrow a]. 
+
+definition sndT \def \lambda A,B:Type.\lambda p: ProdT A B.
+match p with
+[(pairT a b) \Rightarrow b].
\ No newline at end of file