Closed
Description
See #1214 #2095 #2096 and #2099 for further discussion.
There is a design issue at stake here, however: do we use
- defined symbols (the solution adopted in [fixes #1214] Add negated ordering relation symbols systematically to
Relation.Binary.*
#2095 , De-symmetrisingRelation.Binary.Bundles.Preorder._∼_
#2099) syntax
declarations?
pro the first is that we can be more selective about import
s, renaming
, hiding
etc. (needed in those PRs)
pro the second is that it is 'more lightweight', yet somehow more irrevocable.
My current thinking is: defined symbols
UPDATED: one two reasons I may have hesitated to pursue this already to a PR might have been:
- concern about the reception for De-symmetrising
Relation.Binary.Bundles.Preorder._∼_
#2099 (merged) and [fixes #1214] Add negated ordering relation symbols systematically toRelation.Binary.*
#2095 (not yet) before proceeding - more serious: given the proliferation of hand-rolled flipped relations throughout the library, the amount of weeding out that might be required, in order to avoid clashes between the hand-rolled and the machine-made, (still!) seems a bit daunting...