diff options
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 2 | ||||
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 11 |
2 files changed, 6 insertions, 7 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 73baae1..8fd9818 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -275,6 +275,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). + and the same holds for the dual `>=<^d`, `><^d`, the product `>=<^p`, `><^p`, and lexicographic `>=<^l`, `><^l`. The previous meanings can be obtained through `>=<%O x` and `><%O x`. +- In `srnum.v`, + + `>=< y` stands for `[pred x | x >=< y]` ### Renamed diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index 3c88ef0..0244891 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -464,9 +464,6 @@ Notation "< y :> T" := (< (y : T)) (only parsing) : ring_scope. Notation "> y" := (lt y) : ring_scope. Notation "> y :> T" := (> (y : T)) (only parsing) : ring_scope. -Notation ">=< y" := (comparable y) : ring_scope. -Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : ring_scope. - Notation "x <= y" := (le x y) : ring_scope. Notation "x <= y :> T" := ((x : T) <= (y : T)) (only parsing) : ring_scope. Notation "x >= y" := (y <= x) (only parsing) : ring_scope. @@ -490,12 +487,12 @@ Notation "x < y ?<= 'if' C" := (lterif x y C) : ring_scope. Notation "x < y ?<= 'if' C :> R" := ((x : R) < (y : R) ?<= if C) (only parsing) : ring_scope. -Notation ">=< x" := (comparable x) : ring_scope. -Notation ">=< x :> T" := (>=< (x : T)) (only parsing) : ring_scope. +Notation ">=< y" := [pred x | comparable x y] : ring_scope. +Notation ">=< y :> T" := (>=< (y : T)) (only parsing) : ring_scope. Notation "x >=< y" := (comparable x y) : ring_scope. -Notation ">< x" := (fun y => ~~ (comparable x y)) : ring_scope. -Notation ">< x :> T" := (>< (x : T)) (only parsing) : ring_scope. +Notation ">< y" := [pred x | ~~ comparable x y] : ring_scope. +Notation ">< y :> T" := (>< (y : T)) (only parsing) : ring_scope. Notation "x >< y" := (~~ (comparable x y)) : ring_scope. Canonical Rpos_keyed. |