From be797cb755104e7c8709f2602ced5c46c5c1987b Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 22 Aug 2005 08:25:21 +0000 Subject: [PATCH] Added datatypes/constructors.ma --- helm/matita/library/datatypes/constructors.ma | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 helm/matita/library/datatypes/constructors.ma diff --git a/helm/matita/library/datatypes/constructors.ma b/helm/matita/library/datatypes/constructors.ma new file mode 100644 index 000000000..c2bdc566b --- /dev/null +++ b/helm/matita/library/datatypes/constructors.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/datatypes/constructors/". + +inductive void : Set \def. + +inductive Prod (A,B:Set) : Set \def +pair : A \to B \to Prod A B. + +inductive Sum (A,B:Set) : Set \def + inl : A \to Sum A B +| inr : B \to Sum A B. \ No newline at end of file -- 2.39.2