]> matita.cs.unibo.it Git - helm.git/commitdiff
Some more datatypes lifted to Type.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 29 Jan 2007 11:12:43 +0000 (11:12 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 29 Jan 2007 11:12:43 +0000 (11:12 +0000)
helm/software/matita/library/datatypes/constructors.ma

index 3be6bc9d10bf1ef8592e83467d5701848f3e54c2..6d0a68503bb809a72c689be947ef81f38e812c89 100644 (file)
@@ -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 =