From 9962ff269442af5e37c7cefe0bb1582f5ed6af61 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 29 Jan 2007 11:12:43 +0000 Subject: [PATCH] Some more datatypes lifted to Type. --- helm/software/matita/library/datatypes/constructors.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/matita/library/datatypes/constructors.ma b/helm/software/matita/library/datatypes/constructors.ma index 3be6bc9d1..6d0a68503 100644 --- a/helm/software/matita/library/datatypes/constructors.ma +++ b/helm/software/matita/library/datatypes/constructors.ma @@ -19,7 +19,7 @@ inductive void : Set \def. inductive unit : Set ≝ something: unit. -inductive Prod (A,B:Set) : Set \def +inductive Prod (A,B:Type) : Type \def pair : A \to B \to Prod A B. interpretation "Pair construction" 'pair x y = -- 2.39.2