From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Mon, 21 Nov 2005 11:28:31 +0000 (+0000)
Subject: internal quantification fixed
X-Git-Tag: V_0_7_2_3~20
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c5e94d35e8f36f868c5a1f02d80a419bfe802ba1

internal quantification fixed
---

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
index 670211caf..916c91cd8 100644
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma
@@ -30,32 +30,31 @@ record Domain: Type \def {
 coercion qd.
 
 (* internal universal quantification *)
-inductive iall (D:Domain) (P:D \to Prop) : Prop \def
-   | iall_intro: (\forall d:D. cin D d \to P d) \to iall D P.
+inductive dall (D:Domain) (P:D \to Prop) : Prop \def
+   | dall_intro: (\forall d:D. cin D d \to P d) \to dall D P.
 
 (* internal existential quantification *)
-inductive iex (D:Domain) (P:D \to Prop) : Prop \def
-   | iex_intro: \forall d:D. cin D d \land P d \to iex D P.
-(*
+inductive dex (D:Domain) (P:D \to Prop) : Prop \def
+   | dex_intro: \forall d:D. cin D d \land P d \to dex D P.
+
 (* notations **************************************************************)
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "internal for all" 'iall \eta.x =
-  (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/iall.ind#xpointer(1/1) _ x).
+interpretation "internal for all" 'iforall \eta.x =
+  (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/dall.ind#xpointer(1/1) _ x).
 
-notation < "hvbox(\iall ident i opt (: ty) break . p)"
+notation > "hvbox(\iforall ident i opt (: ty) break . p)"
   right associative with precedence 20
-for @{ 'iall ${default
+for @{ 'iforall ${default
   @{\lambda ${ident i} : $ty. $p)}
   @{\lambda ${ident i} . $p}}}.
 
 (*CSC: the URI must disappear: there is a bug now *)
-interpretation "internal exist" 'iexist \eta.x =
-  (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/iex.ind#xpointer(1/1) _ x).
+interpretation "internal exists" 'dexists \eta.x =
+  (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/dex.ind#xpointer(1/1) _ x).
 
-notation < "hvbox(\iexist ident i opt (: ty) break . p)"
+notation > "hvbox(\iexists ident i opt (: ty) break . p)"
   right associative with precedence 20
-for @{ 'iexist ${default
+for @{ 'dexists ${default
   @{\lambda ${ident i} : $ty. $p)}
   @{\lambda ${ident i} . $p}}}.
-*)
\ No newline at end of file
diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma
index 87ecb2780..3cc583f02 100644
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma
@@ -43,12 +43,11 @@ definition sor: \forall D. Subset D \to Subset D \to Subset D \def
 
 (* subset less or equal (inclusion) *) 
 definition sle: \forall D. Subset D \to Subset D \to Prop \def 
-   \lambda D,U1,U2. \forall d. U1 d \to U2 d. 
-(*
+   \lambda D,U1,U2. \iforall d. U1 d \to U2 d. 
+
 (* subset overlap *) 
 definition sover: \forall D. Subset D \to Subset D \to Prop \def 
-   \lambda D,U1,U2. \forall d. U1 d \to U2 d. 
-*)
+   \lambda D,U1,U2. \iexists d. U1 d \land U2 d. 
 
 (* coercions **************************************************************)
 
@@ -65,4 +64,3 @@ coercion domain_of_subset.
 
 (* the full subset of a domain *)
 coercion stop.
-
diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang
index 3241d239e..e99672a35 100644
--- a/helm/matita/matita.lang
+++ b/helm/matita/matita.lang
@@ -172,6 +172,8 @@
      <keyword>lor</keyword>
      <keyword>subst</keyword>
      <keyword>vdash</keyword>
+     <keyword>iforall</keyword>
+     <keyword>iexists</keyword>
   </keyword-list>
 
   <string _name = "String" style = "String" >