Skip to content

Commit d4f2c79

Browse files
committed
further revised CHANGELOG after merge of agda#2099; erroneous prior commit msgs refer to 2114
1 parent ec79e09 commit d4f2c79

File tree

1 file changed

+16
-16
lines changed

1 file changed

+16
-16
lines changed

CHANGELOG.md

+16-16
Original file line numberDiff line numberDiff line change
@@ -822,6 +822,22 @@ Non-backwards compatible changes
822822
IO.Effectful
823823
IO.Instances
824824
```
825+
### (Issue #2096) Introduction of flipped relation symbol for `Relation.Binary.Bundles.Preorder`
826+
827+
* Previously, the relation symbol `_∼_` was (notationally) symmetric, so that its
828+
converse relation could only be discussed *semantically* in terms of `flip _∼_`
829+
in `Relation.Binary.Properties.Preorder`, `Relation.Binary.Construct.Flip.{Ord|EqAndOrd}`
830+
831+
* Now, the symbol `_∼_` has been renamed to a new symbol `_≲_`, with `_≳_`
832+
introduced as a definition in `Relation.Binary.Bundles.Preorder` whose properties
833+
in `Relation.Binary.Properties.Preorder` now refer to it. Partial backwards compatible
834+
has been achieved by redeclaring a deprecated version of the old name in the record.
835+
Therefore, only _declarations_ of `PartialOrder` records will need their field names
836+
updating.
837+
838+
* NB (issue #2098) the corresponding situation regarding the `flip`ped
839+
relation symbols `_≥_`, `_>_` has not (yet) been addressed.
840+
825841
### (Issue #1214) Reorganisation of the introduction of negated relation symbols under `Relation.Binary`
826842

827843
* Previously, negated relation symbols `_≰_` (for `Poset`) and `_≮_` (`TotalOrder`)
@@ -854,22 +870,6 @@ Non-backwards compatible changes
854870
symbols `_≥_`, `_>_` (and their negated versions!) has not (yet) been addressed.
855871
Ditto. the strict ordering relation `_<_` defined in `Relation.Binary.Properties.Poset`...
856872

857-
### (Issue #2096) Introduction of flipped relation symbol for `Relation.Binary.Bundles.Preorder`
858-
859-
* Previously, the relation symbol `_∼_` was (notationally) symmetric, so that its
860-
converse relation could only be discussed *semantically* in terms of `flip _∼_`
861-
in `Relation.Binary.Properties.Preorder`, `Relation.Binary.Construct.Flip.{Ord|EqAndOrd}`
862-
863-
* Now, the symbol `_∼_` has been renamed to a new symbol `_≲_`, with `_≳_`
864-
introduced as a definition in `Relation.Binary.Bundles.Preorder` whose properties
865-
in `Relation.Binary.Properties.Preorder` now refer to it. Partial backwards compatible
866-
has been achieved by redeclaring a deprecated version of the old name in the record.
867-
Therefore, only _declarations_ of `PartialOrder` records will need their field names
868-
updating.
869-
870-
* NB (issue #2098) the corresponding situation regarding the `flip`ped
871-
relation symbols `_≥_`, `_>_` has not (yet) been addressed.
872-
873873
### Standardisation of `insertAt`/`updateAt`/`removeAt`
874874

875875
* Previously, the names and argument order of index-based insertion, update and removal functions for

0 commit comments

Comments
 (0)