Added option datatype. Required (for technicalities/Setoids.ma).

diff --git a/helm/software/matita/library/datatypes/constructors.ma b/helm/software/matita/library/datatypes/constructors.ma
index b91a59e177f71897dbb0bba85a37214cee9c062c..3be6bc9d10bf1ef8592e83467d5701848f3e54c2 100644 (file)
--- a/helm/software/matita/library/datatypes/constructors.ma
+++ b/helm/software/matita/library/datatypes/constructors.ma
@@ -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