some minor fixes

[helm.git] / helm / software / matita / contribs / formal_topology / overlap / categories.ma

diff --git a/helm/software/matita/contribs/formal_topology/overlap/categories.ma b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
index af58968fc14043110c6d220d3858fe2effc0e435..17c5f498f20df3af32034a893a73493076c89e01 100644 (file)
--- a/helm/software/matita/contribs/formal_topology/overlap/categories.ma
+++ b/helm/software/matita/contribs/formal_topology/overlap/categories.ma
@@ -100,6 +100,31 @@ interpretation "setoid3 eq" 'eq x y = (eq_rel3 _ (eq3 _) x y).
 interpretation "setoid2 eq" 'eq x y = (eq_rel2 _ (eq2 _) x y).
 interpretation "setoid1 eq" 'eq x y = (eq_rel1 _ (eq1 _) x y).
 interpretation "setoid eq" 'eq x y = (eq_rel _ (eq _) x y).
+
+notation < "hvbox(a break = \sub 1 b)" non associative with precedence 45
+for @{ 'eq1 $a $b }.
+
+notation < "hvbox(a break = \sub 2 b)" non associative with precedence 45
+for @{ 'eq2 $a $b }.
+
+notation < "hvbox(a break = \sub 3 b)" non associative with precedence 45
+for @{ 'eq3 $a $b }.
+
+notation > "hvbox(a break =_12 b)" non associative with precedence 45
+for @{ eq_rel2 (carr2 (setoid2_of_setoid1 ?)) (eq2 (setoid2_of_setoid1 ?)) $a $b }.
+notation > "hvbox(a break =_0 b)" non associative with precedence 45
+for @{ eq_rel ? (eq ?) $a $b }.
+notation > "hvbox(a break =_1 b)" non associative with precedence 45
+for @{ eq_rel1 ? (eq1 ?) $a $b }.
+notation > "hvbox(a break =_2 b)" non associative with precedence 45
+for @{ eq_rel2 ? (eq2 ?) $a $b }.
+notation > "hvbox(a break =_3 b)" non associative with precedence 45
+for @{ eq_rel3 ? (eq3 ?) $a $b }.
+
+interpretation "setoid3 eq explicit" 'eq3 x y = (eq_rel3 _ (eq3 _) x y).
+interpretation "setoid2 eq explicit" 'eq2 x y = (eq_rel2 _ (eq2 _) x y).
+interpretation "setoid1 eq explicit" 'eq1 x y = (eq_rel1 _ (eq1 _) x y).
+
 interpretation "setoid3 symmetry" 'invert r = (sym3 ____ r).
 interpretation "setoid2 symmetry" 'invert r = (sym2 ____ r).
 interpretation "setoid1 symmetry" 'invert r = (sym1 ____ r).