X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fpermutation.ma;h=4654f33fca7efa46bc1d58daa2ebfea4df0f5f2c;hb=13c10bcf4c938ee43746bce6fb0e160b668e374d;hp=884c18ddc17c0f2a3dafe344c38dabb24160ec38;hpb=c445ba5534cccde19016c92660ab52777af221c0;p=helm.git diff --git a/helm/software/matita/library/nat/permutation.ma b/helm/software/matita/library/nat/permutation.ma index 884c18ddc..4654f33fc 100644 --- a/helm/software/matita/library/nat/permutation.ma +++ b/helm/software/matita/library/nat/permutation.ma @@ -72,12 +72,10 @@ match eqb n i with [ true \Rightarrow i | false \Rightarrow n]]. -notation < "(❲i↹j❳)n" - right associative with precedence 71 +notation < "(❲i↹j❳)n" with precedence 71 for @{ 'transposition $i $j $n}. -notation < "(❲i \atop j❳)n" - right associative with precedence 71 +notation < "(❲i \atop j❳)n" with precedence 71 for @{ 'transposition $i $j $n}. interpretation "natural transposition" 'transposition i j n =