diff options
Diffstat (limited to 'mathcomp/ssreflect/ssrnotations.v')
| -rw-r--r-- | mathcomp/ssreflect/ssrnotations.v | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/mathcomp/ssreflect/ssrnotations.v b/mathcomp/ssreflect/ssrnotations.v index d85fdf8..ae83c2a 100644 --- a/mathcomp/ssreflect/ssrnotations.v +++ b/mathcomp/ssreflect/ssrnotations.v @@ -63,6 +63,9 @@ Reserved Notation "A :\ b" (at level 50, left associativity). Reserved Notation "<< A >>" (at level 0, format "<< A >>"). Reserved Notation "<[ a ] >" (at level 0, format "<[ a ] >"). +(* Reserved notation for the order of an element (group, polynomial, etc) *) +Reserved Notation "#[ x ]" (at level 0, format "#[ x ]"). + (* Reserved notation for centralisers and centers. *) Reserved Notation "''C' [ x ]" (at level 8, format "''C' [ x ]"). Reserved Notation "''C_' A [ x ]" @@ -72,8 +75,8 @@ Reserved Notation "''C_' B ( A )" (at level 8, B at level 2, format "''C_' B ( A )"). Reserved Notation "''Z' ( A )" (at level 8, format "''Z' ( A )"). (* Compatibility with group action centraliser notation. *) -Reserved Notation "''C_' ( A ) [ x ]" (at level 8, only parsing). -Reserved Notation "''C_' ( B ) ( A )" (at level 8, only parsing). +Reserved Notation "''C_' ( A ) [ x ]" (at level 8). +Reserved Notation "''C_' ( B ) ( A )" (at level 8). (* Reserved notation for Euclidean division and divisibility. *) Reserved Notation "m %/ d" (at level 40, no associativity). @@ -101,8 +104,8 @@ Reserved Notation "x <= y ?= 'iff' c" (at level 70, y, c at next level, (* Reserved notation for cast comparison. *) Reserved Notation "x <= y :> T" (at level 70, y at next level). -Reserved Notation "x >= y :> T" (at level 70, y at next level, only parsing). +Reserved Notation "x >= y :> T" (at level 70, y at next level). Reserved Notation "x < y :> T" (at level 70, y at next level). -Reserved Notation "x > y :> T" (at level 70, y at next level, only parsing). +Reserved Notation "x > y :> T" (at level 70, y at next level). Reserved Notation "x <= y ?= 'iff' c :> T" (at level 70, y, c at next level, - format "x '[hv' <= y '/' ?= 'iff' c :> T ']'").
\ No newline at end of file + format "x '[hv' <= y '/' ?= 'iff' c :> T ']'"). |