diff options
| author | Kazuhiko Sakaguchi | 2020-09-10 08:16:56 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-09-17 18:30:03 +0900 |
| commit | 15e57ba36d2b0b96da80679f01c5915137b9ea77 (patch) | |
| tree | b9ddd5062f9a7fa2ca50d14541136a4b59f2c75c | |
| parent | 98315a4e30f746bc01891992ed53559d1a50e863 (diff) | |
Fix big meet and join notations for dual_display, and add `0^d` and `1^d` notations
| -rw-r--r-- | CHANGELOG_UNRELEASED.md | 4 | ||||
| -rw-r--r-- | mathcomp/ssreflect/order.v | 13 |
2 files changed, 17 insertions, 0 deletions
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 716c0ae..95c0d63 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -133,6 +133,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). deprecated and will be removed two releases from now. - in `eqtype.v` new lemmas `contra_not_neq`, `contra_eq_not`. +- in `order.v`, new notations `0^d` and `1^d` for bottom and top elements of + dual lattices. ### Changed @@ -157,6 +159,8 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). `big_uncond` (cf Added) but it will be renamed `big_mkcond` in the next release. +- in `order.v`, `\join^d_` and `\meet^d_` notations are now properly specialized + for `dual_display`. ### Renamed diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v index 846885e..da0e4d7 100644 --- a/mathcomp/ssreflect/order.v +++ b/mathcomp/ssreflect/order.v @@ -468,6 +468,9 @@ Reserved Notation "A `|^d` B" (at level 52, left associativity). Reserved Notation "A `\^d` B" (at level 50, left associativity). Reserved Notation "~^d` A" (at level 35, right associativity). +Reserved Notation "0^d" (at level 0). +Reserved Notation "1^d" (at level 0). + (* 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). @@ -2551,6 +2554,16 @@ Notation "x ><^d y" := (~~ (><^d%O x y)) : order_scope. Notation "x `&^d` y" := (dual_meet x y) : order_scope. Notation "x `|^d` y" := (dual_join x y) : order_scope. +Notation "0^d" := dual_bottom : order_scope. +Notation "1^d" := dual_top : order_scope. + +(* The following Local Notations are here to define the \join^d_ and \meet^d_ *) +(* notations later. Do not remove them. *) +Local Notation "0" := dual_bottom. +Local Notation "1" := dual_top. +Local Notation join := dual_join. +Local Notation meet := dual_meet. + Notation "\join^d_ ( i <- r | P ) F" := (\big[join/0]_(i <- r | P%B) F%O) : order_scope. Notation "\join^d_ ( i <- r ) F" := |