A compiling version of the library.

[helm.git] / matita / library / datatypes / constructors.ma

diff --git a/matita/library/datatypes/constructors.ma b/matita/library/datatypes/constructors.ma
index 2ac1cb376804ad8e89dbd2a805cbd9c1c1284065..3f74db5ad85cfb8b7e9ce99d414471fe53f88f3b 100644 (file)
--- 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