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: make_still_working~6505
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9725ce192edbff9cc1c0af04a60065c1bfd31ca6;p=helm.git

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 b91a59e17..3be6bc9d1 100644
--- 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