diff options
| -rw-r--r-- | mathcomp/algebra/matrix.v | 28 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrint.v | 30 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 5 | ||||
| -rw-r--r-- | mathcomp/character/classfun.v | 14 | ||||
| -rw-r--r-- | mathcomp/field/cyclotomic.v | 2 | ||||
| -rw-r--r-- | mathcomp/fingroup/fingroup.v | 1 | ||||
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 18 | ||||
| -rw-r--r-- | mathcomp/ssreflect/generic_quotient.v | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 111 | ||||
| -rw-r--r-- | mathcomp/ssreflect/ssrnotations.v | 13 |
10 files changed, 104 insertions, 122 deletions
diff --git a/mathcomp/algebra/matrix.v b/mathcomp/algebra/matrix.v index 21730c3..a2b874a 100644 --- a/mathcomp/algebra/matrix.v +++ b/mathcomp/algebra/matrix.v @@ -148,19 +148,19 @@ Local Open Scope ring_scope. Reserved Notation "''M_' n" (at level 8, n at level 2, format "''M_' n"). Reserved Notation "''rV_' n" (at level 8, n at level 2, format "''rV_' n"). Reserved Notation "''cV_' n" (at level 8, n at level 2, format "''cV_' n"). -Reserved Notation "''M_' ( n )" (at level 8, only parsing). +Reserved Notation "''M_' ( n )" (at level 8). (* only parsing *) Reserved Notation "''M_' ( m , n )" (at level 8, format "''M_' ( m , n )"). -Reserved Notation "''M[' R ]_ n" (at level 8, n at level 2, only parsing). -Reserved Notation "''rV[' R ]_ n" (at level 8, n at level 2, only parsing). -Reserved Notation "''cV[' R ]_ n" (at level 8, n at level 2, only parsing). -Reserved Notation "''M[' R ]_ ( n )" (at level 8, only parsing). -Reserved Notation "''M[' R ]_ ( m , n )" (at level 8, only parsing). +Reserved Notation "''M[' R ]_ n" (at level 8, n at level 2). (* only parsing *) +Reserved Notation "''rV[' R ]_ n" (at level 8, n at level 2). (* only parsing *) +Reserved Notation "''cV[' R ]_ n" (at level 8, n at level 2). (* only parsing *) +Reserved Notation "''M[' R ]_ ( n )" (at level 8). (* only parsing *) +Reserved Notation "''M[' R ]_ ( m , n )" (at level 8). (* only parsing *) Reserved Notation "\matrix_ i E" (at level 36, E at level 36, i at level 2, format "\matrix_ i E"). Reserved Notation "\matrix_ ( i < n ) E" - (at level 36, E at level 36, i, n at level 50, only parsing). + (at level 36, E at level 36, i, n at level 50). (* only parsing *) Reserved Notation "\matrix_ ( i , j ) E" (at level 36, E at level 36, i, j at level 50, format "\matrix_ ( i , j ) E"). @@ -168,19 +168,19 @@ Reserved Notation "\matrix[ k ]_ ( i , j ) E" (at level 36, E at level 36, i, j at level 50, format "\matrix[ k ]_ ( i , j ) E"). Reserved Notation "\matrix_ ( i < m , j < n ) E" - (at level 36, E at level 36, i, m, j, n at level 50, only parsing). + (at level 36, E at level 36, i, m, j, n at level 50). (* only parsing *) Reserved Notation "\matrix_ ( i , j < n ) E" - (at level 36, E at level 36, i, j, n at level 50, only parsing). + (at level 36, E at level 36, i, j, n at level 50). (* only parsing *) Reserved Notation "\row_ j E" (at level 36, E at level 36, j at level 2, format "\row_ j E"). Reserved Notation "\row_ ( j < n ) E" - (at level 36, E at level 36, j, n at level 50, only parsing). + (at level 36, E at level 36, j, n at level 50). (* only parsing *) Reserved Notation "\col_ j E" (at level 36, E at level 36, j at level 2, format "\col_ j E"). Reserved Notation "\col_ ( j < n ) E" - (at level 36, E at level 36, j, n at level 50, only parsing). + (at level 36, E at level 36, j, n at level 50). (* only parsing *) Reserved Notation "x %:M" (at level 8, format "x %:M"). Reserved Notation "A *m B" (at level 40, left associativity, format "A *m B"). @@ -248,8 +248,8 @@ Notation "''cV_' n" := 'M_(n, 1) : type_scope. Notation "''M_' n" := 'M_(n, n) : type_scope. Notation "''M_' ( n )" := 'M_n (only parsing) : type_scope. -Notation "\matrix[ k ]_ ( i , j ) E" := (matrix_of_fun k (fun i j => E)) - (at level 36, E at level 36, i, j at level 50): ring_scope. +Notation "\matrix[ k ]_ ( i , j ) E" := (matrix_of_fun k (fun i j => E)) : + ring_scope. Notation "\matrix_ ( i < m , j < n ) E" := (@matrix_of_fun _ m n matrix_key (fun i j => E)) (only parsing) : ring_scope. @@ -1579,7 +1579,7 @@ Qed. Lemma mul_delta_mx_cond m n p (j1 j2 : 'I_n) (i1 : 'I_m) (k2 : 'I_p) : delta_mx i1 j1 *m delta_mx j2 k2 = delta_mx i1 k2 *+ (j1 == j2). Proof. -apply/matrixP=> i k; rewrite !mxE (bigD1 j1) //=. +apply/matrixP => i k; rewrite !mxE (bigD1 j1) //=. rewrite mulmxnE !mxE !eqxx andbT -natrM -mulrnA !mulnb !andbA andbAC. by rewrite big1 ?addr0 // => j; rewrite !mxE andbC -natrM; move/negPf->. Qed. diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v index 3903609..f54a957 100644 --- a/mathcomp/algebra/ssrint.v +++ b/mathcomp/algebra/ssrint.v @@ -40,6 +40,16 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Reserved Notation "n %:Z" (at level 2, left associativity, format "n %:Z"). +Reserved Notation "n = m :> 'in' 't'" + (at level 70, m at next level, format "n = m :> 'in' 't'"). +Reserved Notation "n == m :> 'in' 't'" + (at level 70, m at next level, format "n == m :> 'in' 't'"). +Reserved Notation "n != m :> 'in' 't'" + (at level 70, m at next level, format "n != m :> 'in' 't'"). +Reserved Notation "n <> m :> 'in' 't'" + (at level 70, m at next level, format "n <> m :> 'in' 't'"). + Import Order.TTheory GRing.Theory Num.Theory. Delimit Scope int_scope with Z. Local Open Scope int_scope. @@ -50,19 +60,13 @@ Variant int : Set := Posz of nat | Negz of nat. (* the Coq module system. *) (* Coercion Posz : nat >-> int. *) -Notation "n %:Z" := (Posz n) - (at level 2, left associativity, format "n %:Z", only parsing) : int_scope. -Notation "n %:Z" := (Posz n) - (at level 2, left associativity, format "n %:Z", only parsing) : ring_scope. - -Notation "n = m :> 'in' 't'" := (Posz n = Posz m) - (at level 70, m at next level, format "n = m :> 'in' 't'") : ring_scope. -Notation "n == m :> 'in' 't'" := (Posz n == Posz m) - (at level 70, m at next level, format "n == m :> 'in' 't'") : ring_scope. -Notation "n != m :> 'in' 't'" := (Posz n != Posz m) - (at level 70, m at next level, format "n != m :> 'in' 't'") : ring_scope. -Notation "n <> m :> 'in' 't'" := (Posz n <> Posz m) - (at level 70, m at next level, format "n <> m :> 'in' 't'") : ring_scope. +Notation "n %:Z" := (Posz n) (only parsing) : int_scope. +Notation "n %:Z" := (Posz n) (only parsing) : ring_scope. + +Notation "n = m :> 'in' 't'" := (Posz n = Posz m) : ring_scope. +Notation "n == m :> 'in' 't'" := (Posz n == Posz m) : ring_scope. +Notation "n != m :> 'in' 't'" := (Posz n != Posz m) : ring_scope. +Notation "n <> m :> 'in' 't'" := (Posz n <> Posz m) : ring_scope. Definition natsum_of_int (m : int) : nat + nat := match m with Posz p => inl _ p | Negz n => inr _ n end. diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 3bae08e..6198b44 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -1579,7 +1579,7 @@ Arguments ler01 {R}. Arguments ltr01 {R}. Arguments normr_idP {R x}. Arguments normr0P {R V v}. -Hint Resolve @ler01 @ltr01 ltr0Sn ler0n : core. +Hint Resolve ler01 ltr01 ltr0Sn ler0n : core. Hint Extern 0 (is_true (0 <= norm _)) => exact: normr_ge0 : core. Section NumDomainOperationTheory. @@ -3821,7 +3821,8 @@ Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F] Variable R : realDomainType. Implicit Types x y z t : R. -Hint Resolve (@num_real R) : core. +Let numR_real := @num_real R. +Hint Resolve numR_real : core. Lemma sgr_cp0 x : ((sg x == 1) = (0 < x)) * diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v index fc19eba..9c4557a 100644 --- a/mathcomp/character/classfun.v +++ b/mathcomp/character/classfun.v @@ -98,16 +98,16 @@ Delimit Scope cfun_scope with CF. Reserved Notation "''CF' ( G , A )" (at level 8, format "''CF' ( G , A )"). Reserved Notation "''CF' ( G )" (at level 8, format "''CF' ( G )"). Reserved Notation "''1_' G" (at level 8, G at level 2, format "''1_' G"). -Reserved Notation "''Res[' H , G ]" (at level 8, only parsing). +Reserved Notation "''Res[' H , G ]" (at level 8). (* only parsing *) Reserved Notation "''Res[' H ]" (at level 8, format "''Res[' H ]"). -Reserved Notation "''Res'" (at level 8, only parsing). -Reserved Notation "''Ind[' G , H ]" (at level 8, only parsing). -Reserved Notation "''Ind[' G ]" (at level 8, format "''Ind[' G ]"). -Reserved Notation "''Ind'" (at level 8, only parsing). -Reserved Notation "'[ phi , psi ]_ G" (at level 2, only parsing). +Reserved Notation "''Res'" (at level 8). (* only parsing *) +Reserved Notation "''Ind[' G , H ]" (at level 8). (* only parsing *) +Reserved Notation "''Ind[' G ]" (at level 8). (* only "''Ind[' G ]" *) +Reserved Notation "''Ind'" (at level 8). (* only parsing *) +Reserved Notation "'[ phi , psi ]_ G" (at level 2). (* only parsing *) Reserved Notation "'[ phi , psi ]" (at level 2, format "'[hv' ''[' phi , '/ ' psi ] ']'"). -Reserved Notation "'[ phi ]_ G" (at level 2, only parsing). +Reserved Notation "'[ phi ]_ G" (at level 2). (* only parsing *) Reserved Notation "'[ phi ]" (at level 2, format "''[' phi ]"). Reserved Notation "phi ^u" (at level 3, format "phi ^u"). diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v index ce8c5b7..658258c 100644 --- a/mathcomp/field/cyclotomic.v +++ b/mathcomp/field/cyclotomic.v @@ -117,7 +117,7 @@ Local Notation pZtoC := (map_poly ZtoC). Local Notation pQtoC := (map_poly ratr). Local Definition algC_intr_inj := @intr_inj [numDomainType of algC]. -Local Hint Resolve algC_intr_inj. +Local Hint Resolve algC_intr_inj : core. Local Notation QtoC_M := (ratr_rmorphism [numFieldType of algC]). Lemma C_prim_root_exists n : (n > 0)%N -> {z : algC | n.-primitive_root z}. diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v index b90b35a..c828225 100644 --- a/mathcomp/fingroup/fingroup.v +++ b/mathcomp/fingroup/fingroup.v @@ -170,7 +170,6 @@ Reserved Notation "''N' ( A )" (at level 8, format "''N' ( A )"). Reserved Notation "''N_' G ( A )" (at level 8, G at level 2, format "''N_' G ( A )"). Reserved Notation "A <| B" (at level 70, no associativity). -Reserved Notation "#[ x ]" (at level 0, format "#[ x ]"). Reserved Notation "A <*> B" (at level 40, left associativity). Reserved Notation "[ ~: A1 , A2 , .. , An ]" (at level 0, format "[ ~: '[' A1 , '/' A2 , '/' .. , '/' An ']' ]"). diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index de03369..5f1b7d7 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -158,11 +158,9 @@ Reserved Notation "\sum_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \sum_ ( i | P ) '/ ' F ']'"). Reserved Notation "\sum_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). (* only parsing *) Reserved Notation "\sum_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). (* only parsing *) Reserved Notation "\sum_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \sum_ ( i < n | P ) '/ ' F ']'"). @@ -195,11 +193,9 @@ Reserved Notation "\max_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \max_ ( i | P ) '/ ' F ']'"). Reserved Notation "\max_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). (* only parsing *) Reserved Notation "\max_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). (* only parsing *) Reserved Notation "\max_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \max_ ( i < n | P ) '/ ' F ']'"). @@ -232,11 +228,9 @@ Reserved Notation "\prod_ ( i | P ) F" (at level 36, F at level 36, i at level 50, format "'[' \prod_ ( i | P ) '/ ' F ']'"). Reserved Notation "\prod_ ( i : t | P ) F" - (at level 36, F at level 36, i at level 50, - only parsing). + (at level 36, F at level 36, i at level 50). (* only parsing *) Reserved Notation "\prod_ ( i : t ) F" - (at level 36, F at level 36, i at level 50, - only parsing). + (at level 36, F at level 36, i at level 50). (* only parsing *) Reserved Notation "\prod_ ( i < n | P ) F" (at level 36, F at level 36, i, n at level 50, format "'[' \prod_ ( i < n | P ) '/ ' F ']'"). diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v index 5ec4037..c8b1490 100644 --- a/mathcomp/ssreflect/generic_quotient.v +++ b/mathcomp/ssreflect/generic_quotient.v @@ -101,8 +101,8 @@ Reserved Notation "x != y %[mod_eq e ]" (at level 70, y at next level, no associativity, format "'[hv ' x '/' != y '/' %[mod_eq e ] ']'"). Reserved Notation "x <> y %[mod_eq e ]" (at level 70, y at next level, no associativity, format "'[hv ' x '/' <> y '/' %[mod_eq e ] ']'"). -Reserved Notation "{eq_quot e }" (at level 0, e at level 0, - format "{eq_quot e }", only parsing). +Reserved Notation "{eq_quot e }" + (at level 0, e at level 0, format "{eq_quot e }"). Delimit Scope quotient_scope with qT. Local Open Scope quotient_scope. diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 10a26f1..dd9099b 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -415,13 +415,13 @@ Reserved Notation "~` A" (at level 35, right associativity). (* Notations for dual partial and total order *) Reserved Notation "x <=^d y" (at level 70, y at next level). -Reserved Notation "x >=^d y" (at level 70, y at next level, only parsing). +Reserved Notation "x >=^d y" (at level 70, y at next level). Reserved Notation "x <^d y" (at level 70, y at next level). -Reserved Notation "x >^d y" (at level 70, y at next level, only parsing). +Reserved Notation "x >^d y" (at level 70, y at next level). Reserved Notation "x <=^d y :> T" (at level 70, y at next level). -Reserved Notation "x >=^d y :> T" (at level 70, y at next level, only parsing). +Reserved Notation "x >=^d y :> T" (at level 70, y at next level). Reserved Notation "x <^d y :> T" (at level 70, y at next level). -Reserved Notation "x >^d y :> T" (at level 70, y at next level, only parsing). +Reserved Notation "x >^d y :> T" (at level 70, y at next level). Reserved Notation "<=^d y" (at level 35). Reserved Notation ">=^d y" (at level 35). Reserved Notation "<^d y" (at level 35). @@ -454,13 +454,13 @@ Reserved Notation "~^d` A" (at level 35, right associativity). (* Reserved notations for product ordering of prod or seq *) Reserved Notation "x <=^p y" (at level 70, y at next level). -Reserved Notation "x >=^p y" (at level 70, y at next level, only parsing). +Reserved Notation "x >=^p y" (at level 70, y at next level). Reserved Notation "x <^p y" (at level 70, y at next level). -Reserved Notation "x >^p y" (at level 70, y at next level, only parsing). +Reserved Notation "x >^p y" (at level 70, y at next level). Reserved Notation "x <=^p y :> T" (at level 70, y at next level). -Reserved Notation "x >=^p y :> T" (at level 70, y at next level, only parsing). +Reserved Notation "x >=^p y :> T" (at level 70, y at next level). Reserved Notation "x <^p y :> T" (at level 70, y at next level). -Reserved Notation "x >^p y :> T" (at level 70, y at next level, only parsing). +Reserved Notation "x >^p y :> T" (at level 70, y at next level). Reserved Notation "<=^p y" (at level 35). Reserved Notation ">=^p y" (at level 35). Reserved Notation "<^p y" (at level 35). @@ -493,13 +493,13 @@ Reserved Notation "~^p` A" (at level 35, right associativity). (* Reserved notations for lexicographic ordering of prod or seq *) Reserved Notation "x <=^l y" (at level 70, y at next level). -Reserved Notation "x >=^l y" (at level 70, y at next level, only parsing). +Reserved Notation "x >=^l y" (at level 70, y at next level). Reserved Notation "x <^l y" (at level 70, y at next level). -Reserved Notation "x >^l y" (at level 70, y at next level, only parsing). +Reserved Notation "x >^l y" (at level 70, y at next level). Reserved Notation "x <=^l y :> T" (at level 70, y at next level). -Reserved Notation "x >=^l y :> T" (at level 70, y at next level, only parsing). +Reserved Notation "x >=^l y :> T" (at level 70, y at next level). Reserved Notation "x <^l y :> T" (at level 70, y at next level). -Reserved Notation "x >^l y :> T" (at level 70, y at next level, only parsing). +Reserved Notation "x >^l y :> T" (at level 70, y at next level). Reserved Notation "<=^l y" (at level 35). Reserved Notation ">=^l y" (at level 35). Reserved Notation "<^l y" (at level 35). @@ -546,11 +546,9 @@ Reserved Notation "\gcd_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \gcd_ ( i | P ) '/ ' F ']'"). Reserved Notation "\gcd_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\gcd_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\gcd_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \gcd_ ( i < n | P ) '/ ' F ']'"). @@ -583,11 +581,9 @@ Reserved Notation "\lcm_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \lcm_ ( i | P ) '/ ' F ']'"). Reserved Notation "\lcm_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\lcm_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\lcm_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \lcm_ ( i < n | P ) '/ ' F ']'"). @@ -626,11 +622,9 @@ Reserved Notation "\meet_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \meet_ ( i | P ) '/ ' F ']'"). Reserved Notation "\meet_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\meet_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\meet_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \meet_ ( i < n | P ) '/ ' F ']'"). @@ -663,11 +657,9 @@ Reserved Notation "\join_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \join_ ( i | P ) '/ ' F ']'"). Reserved Notation "\join_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\join_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\join_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \join_ ( i < n | P ) '/ ' F ']'"). @@ -700,11 +692,9 @@ Reserved Notation "\min_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \min_ ( i | P ) '/ ' F ']'"). Reserved Notation "\min_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\min_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\min_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \min_ ( i < n | P ) '/ ' F ']'"). @@ -737,11 +727,9 @@ Reserved Notation "\max_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \max_ ( i | P ) '/ ' F ']'"). Reserved Notation "\max_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\max_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\max_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \max_ ( i < n | P ) '/ ' F ']'"). @@ -774,11 +762,9 @@ Reserved Notation "\meet^d_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \meet^d_ ( i | P ) '/ ' F ']'"). Reserved Notation "\meet^d_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\meet^d_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\meet^d_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \meet^d_ ( i < n | P ) '/ ' F ']'"). @@ -811,11 +797,9 @@ Reserved Notation "\join^d_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \join^d_ ( i | P ) '/ ' F ']'"). Reserved Notation "\join^d_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\join^d_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\join^d_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \join^d_ ( i < n | P ) '/ ' F ']'"). @@ -848,11 +832,9 @@ Reserved Notation "\min^d_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \min^d_ ( i | P ) '/ ' F ']'"). Reserved Notation "\min^d_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\min^d_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\min^d_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \min^d_ ( i < n | P ) '/ ' F ']'"). @@ -885,11 +867,9 @@ Reserved Notation "\max^d_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \max^d_ ( i | P ) '/ ' F ']'"). Reserved Notation "\max^d_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\max^d_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\max^d_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \max^d_ ( i < n | P ) '/ ' F ']'"). @@ -922,11 +902,9 @@ Reserved Notation "\meet^p_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \meet^p_ ( i | P ) '/ ' F ']'"). Reserved Notation "\meet^p_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\meet^p_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\meet^p_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \meet^p_ ( i < n | P ) '/ ' F ']'"). @@ -959,11 +937,9 @@ Reserved Notation "\join^p_ ( i | P ) F" (at level 41, F at level 41, i at level 50, format "'[' \join^p_ ( i | P ) '/ ' F ']'"). Reserved Notation "\join^p_ ( i : t | P ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\join^p_ ( i : t ) F" - (at level 41, F at level 41, i at level 50, - only parsing). + (at level 41, F at level 41, i at level 50). Reserved Notation "\join^p_ ( i < n | P ) F" (at level 41, F at level 41, i, n at level 50, format "'[' \join^p_ ( i < n | P ) '/ ' F ']'"). @@ -3160,7 +3136,9 @@ Context {T : porderType disp} {T' : porderType disp'}. Implicit Types (m n p : nat) (x y z : T) (u v w : T'). Variables (D D' : {pred T}) (f : T -> T'). -Hint Resolve lexx lt_neqAle (@le_anti _ T) (@le_anti _ T') lt_def : core. +Let leT_anti := @le_anti _ T. +Let leT'_anti := @le_anti _ T'. +Hint Resolve lexx lt_neqAle lt_def : core. Let ge_antiT : antisymmetric (>=%O : rel T). Proof. by move=> ? ? /le_anti. Qed. @@ -3741,8 +3719,12 @@ Context {T : orderType disp} {T' : porderType disp'}. Variables (D : {pred T}) (f : T -> T'). Implicit Types (x y z : T) (u v w : T'). -Hint Resolve (@le_anti _ T) (@le_anti _ T') (@lt_neqAle _ T) : core. -Hint Resolve (@lt_neqAle _ T') (@lt_def _ T) (@le_total _ T) : core. +Let leT_anti := @le_anti _ T. +Let leT'_anti := @le_anti _ T'. +Let ltT_neqAle := @lt_neqAle _ T. +Let ltT'_neqAle := @lt_neqAle _ T'. +Let ltT_def := @lt_def _ T. +Let leT_total := @le_total _ T. Lemma le_mono : {homo f : x y / x < y} -> {mono f : x y / x <= y}. Proof. exact: total_homo_mono. Qed. @@ -4869,8 +4851,7 @@ Notation "[ 'porderMixin' 'of' T 'by' <: ]" := Notation "[ 'totalOrderMixin' 'of' T 'by' <: ]" := (sub_TotalOrderMixin _ : totalPOrderMixin [porderType of T]) - (at level 0, format "[ 'totalOrderMixin' 'of' T 'by' <: ]", - only parsing) : form_scope. + (at level 0, only parsing) : form_scope. Canonical sub_POrderType. Canonical sub_LatticeType. 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 ']'"). |