From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sat, 27 Jan 2007 16:32:56 +0000 (+0000)
Subject: Added option datatype. Required (for technicalities/Setoids.ma).
X-Git-Tag: 0.4.95@7852~646
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ceede617914347a8e39f4bddd3f4fc65efb0069e;p=helm.git

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

diff --git a/matita/library/datatypes/constructors.ma b/matita/library/datatypes/constructors.ma
index b91a59e17..3be6bc9d1 100644
--- a/matita/library/datatypes/constructors.ma
+++ b/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