From 9725ce192edbff9cc1c0af04a60065c1bfd31ca6 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 27 Jan 2007 16:32:56 +0000 Subject: [PATCH] Added option datatype. Required (for technicalities/Setoids.ma). --- helm/software/matita/library/datatypes/constructors.ma | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 -- 2.39.2