From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 16 Nov 2005 18:09:57 +0000 (+0000)
Subject: predicative subsets started
X-Git-Tag: V_0_7_2_3~60
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=e872b5a4773aba12d17595eec45ca713c846e26d

predicative subsets started
---

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
index e4ee22311..b375c69ad 100644
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
@@ -30,7 +30,7 @@ include "coq.ma".
      of the aceq predicate given inside the category. Then we prove the 
      properties of the equality that usually are axiomatized inside the 
      category structure. This makes categories easier to use
-     *) 
+*) 
 
 record AC: Type \def {
    ac: Type;
diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma
index 2fb07bd64..0fd993411 100644
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma
@@ -24,7 +24,7 @@ record QD: Type \def {
 }.
 
 coercion qd.
-
+(*
 inductive iall (D:QD) (P:D \to Prop) : Prop \def
    | iall_intro: (\forall (a:D). acin D a \to P a) \to iall D P.
-   
+*)   
diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma
new file mode 100644
index 000000000..579708e6f
--- /dev/null
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma
@@ -0,0 +1,27 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/subsets_defs".
+
+include "qd_defs.ma".
+
+(* SUBSETS
+   - We use predicative subsets coded as propositional functions
+     according to G.Sambin and S.Valentini "Toolbox" 
+*)
+
+definition Subset \def \forall (D:QD). D \to Prop.
+
+alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
+definition stop \def \lambda (D:QD). \lambda (a:(ac (qd D))). True.