backport of WIP on \lambda\delta to matita 0.99.3

[helm.git] / matita / matita / lib / formal_topology / o-algebra.ma

diff --git a/matita/matita/lib/formal_topology/o-algebra.ma b/matita/matita/lib/formal_topology/o-algebra.ma
index f84249343f0c8b875a75f6bd5fdb1f8672646b9b..61a784605dfbaec75c5254a6e6fa1463bcc466c0 100644 (file)
--- a/matita/matita/lib/formal_topology/o-algebra.ma
+++ b/matita/matita/lib/formal_topology/o-algebra.ma
@@ -12,8 +12,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basics/core_notation/comprehension_2.ma".
 include "formal_topology/categories.ma".
-
+(*
 inductive bool : Type[0] := true : bool | false : bool.
 
 lemma BOOL : objs1 SET.
@@ -100,11 +101,11 @@ for @{ 'overlap $a $b}.
 interpretation "o-algebra overlap" 'overlap a b = (fun21 ??? (oa_overlap ?) a b).
 
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)" 
-non associative with precedence 50 for @{ 'oa_meet $p }.
+non associative with precedence 55 for @{ 'oa_meet $p }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈  I) break term 90 p)" 
-non associative with precedence 50 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }.
+non associative with precedence 55 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }.
 
-notation > "hovbox(∧ f)" non associative with precedence 60
+notation > "hovbox(∧ f)" non associative with precedence 65
 for @{ 'oa_meet $f }.
 interpretation "o-algebra meet" 'oa_meet f = 
   (fun12 ?? (oa_meet ??) f).
@@ -112,11 +113,11 @@ interpretation "o-algebra meet with explicit function" 'oa_meet_mk f =
   (fun12 ?? (oa_meet ??) (mk_unary_morphism1 ?? f ?)).
 
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" 
-non associative with precedence 50 for @{ 'oa_join $p }.
+non associative with precedence 55 for @{ 'oa_join $p }.
 notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈  I) break term 90 p)" 
-non associative with precedence 50 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }.
+non associative with precedence 55 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }.
 
-notation > "hovbox(∨ f)" non associative with precedence 60
+notation > "hovbox(∨ f)" non associative with precedence 65
 for @{ 'oa_join $f }.
 interpretation "o-algebra join" 'oa_join f = 
   (fun12 ?? (oa_join ??) f).
@@ -166,7 +167,7 @@ non associative with precedence 49 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }.
 notation < "hovbox(a ∨ b)" left associative with precedence 49
 for @{ 'oa_join_mk (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
 
-notation > "hovbox(∨ f)" non associative with precedence 59
+notation > "hovbox(∨ f)" non associative with precedence 64
 for @{ 'oa_join $f }.
 notation > "hovbox(a ∨ b)" left associative with precedence 49
 for @{ 'oa_join (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }.
@@ -440,3 +441,4 @@ qed.
 lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
  intros; split; intro; apply oa_overlap_sym; assumption.
 qed.
+*)