From e872b5a4773aba12d17595eec45ca713c846e26d Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 16 Nov 2005 18:09:57 +0000
Subject: [PATCH] predicative subsets started

---
 .../contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma  |  2 +-
 .../contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma  |  4 +--
 .../PREDICATIVE-TOPOLOGY/subsets_defs.ma      | 27 +++++++++++++++++++
 3 files changed, 30 insertions(+), 3 deletions(-)
 create mode 100644 helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma

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.
-- 
2.39.2