]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/matita/nlibrary/sets/setoids.ma
update in delayed_updating
[helm.git] / matita / matita / nlibrary / sets / setoids.ma
index e40dad6f6d20e4e3a1f7624b6f28b5d6056a6ef3..f5483607424a75d4e8031d4b6de88ea380301e4d 100644 (file)
@@ -41,9 +41,9 @@ notation > "hvbox(a break =_0 b)" non associative with precedence 45
 for @{ eq_rel ? (eq0 ?) $a $b }.
 
 interpretation "setoid symmetry" 'invert r = (sym ???? r).
-notation ".= r" with precedence 50 for @{'trans $r}.
+notation ".= r" with precedence 55 for @{'trans $r}.
 interpretation "trans" 'trans r = (trans ????? r).
-notation > ".=_0 r" with precedence 50 for @{'trans_x0 $r}.
+notation > ".=_0 r" with precedence 55 for @{'trans_x0 $r}.
 interpretation "trans_x0" 'trans_x0 r = (trans ????? r).
 
 nrecord unary_morphism (A,B: setoid) : Type[0] ≝ {