]> matita.cs.unibo.it Git - helm.git/commitdiff
Added option datatype. Required (for technicalities/Setoids.ma).
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 27 Jan 2007 16:32:56 +0000 (16:32 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 27 Jan 2007 16:32:56 +0000 (16:32 +0000)
matita/library/datatypes/constructors.ma

index b91a59e177f71897dbb0bba85a37214cee9c062c..3be6bc9d10bf1ef8592e83467d5701848f3e54c2 100644 (file)
@@ -72,4 +72,8 @@ match p with
 
 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
+[(pairT a b) \Rightarrow b].
+
+inductive option (A:Type) : Type ≝
+   None : option A
+ | Some : A → option A.
\ No newline at end of file