Skip to content

Commit 5575ab4

Browse files
committed
revised forward pointer to issues agda#2096 agda#2098
1 parent 6ba0381 commit 5575ab4

File tree

1 file changed

+7
-7
lines changed

1 file changed

+7
-7
lines changed

CHANGELOG.md

+7-7
Original file line numberDiff line numberDiff line change
@@ -791,13 +791,13 @@ Non-backwards compatible changes
791791
only on the the underlying `Structures` such as `IsPartialOrder` etc., are unable
792792
to make use of the new symbols.
793793

794-
* NB the corresponding situation regarding the `flip`ped relation symbols `_≥_`,
795-
`_>_` (and their negated versions!) has not (yet) been addressed; to develop
796-
a parallel architecture to that above, there would need to be a suitable symbol
797-
for the flipped relation `_∼_` (and its negation!) in `Relation.Bundles.Preorder`,
798-
now handled purely semantically via `flip ∼` in `Relation.Binary.Properties.Preorder`,
799-
`Relation.Binary.Construct.Flip.{Ord|EqAndOrd}` etc. Similarly, for the strict
800-
ordering relation `_<_` defined in `Relation.Binary.Properties.Poset`...
794+
* NB (issues #2096 #2098) the corresponding situation regarding the `flip`ped
795+
relation symbols `_≥_`, `_>_` (and their negated versions!) has not (yet)
796+
been addressed; to develop a parallel architecture to that above, there
797+
would need to be a suitable symbol for the flipped relation `_∼_` (and its negation!)
798+
in `Relation.Bundles.Preorder`, currently handled purely semantically via `flip ∼`
799+
in `Relation.Binary.Properties.Preorder`, `Relation.Binary.Construct.Flip.{Ord|EqAndOrd}`
800+
etc. Similarly, for the strict ordering relation `_<_` defined in `Relation.Binary.Properties.Poset`...
801801

802802
### Other
803803

0 commit comments

Comments
 (0)