-
Notifications
You must be signed in to change notification settings - Fork 264
Use consistent names for Decidable combinators (#2842 redux) #2846
Copy link
Copy link
Open
Description
As #2843 makes clear, this issue proliferates beyond the Relation.Nullary.Decidable.Core combinators, but how to handle that (downstream!) should probably be separate issues (incl. eg. #2845 ), but with callbacks to #2842 ...
UPDATED: ugh. shopping list needs revision, because GitHub isn't linking to the relevant comments correctly?!
Shopping list:
-
≡?: [ fix ]Relation.Nullary.Decidable.Corenames for combinators #2843 (comment) FIXED in [ breaking ] change fieldname_≟_to_≈?_inIsDecEquivalence#2952 -
_∩?_: [ fix ]Relation.Nullary.Decidable.Corenames for combinators #2843 (comment) See [ rename ] decidability forRelation.Binary.Construct.{Intersection|Union}` #2955 and for_∪?_as well -
pointwise?: [ fix ]Relation.Nullary.Decidable.Corenames for combinators #2843 (comment) on balance,- I (used to) think that 'fixing' this one would be a jarring naming inconsistency wrt all the other combinators defined in that module
Pointwiseis already arguably a problem wrt discoverability, and adding another cognate name helps sediment that decision; UPDATED so now consider changing the names altogether!- UPDATED: see [ refactor ] name of
Data.Product.Relation.Binary.Pointwise.NonDependent.×-decidable#2958
-
×?inData.Product.Relation.Binary.Lex.Strict: [ fix ]Relation.Nullary.Decidable.Corenames for combinators #2843 (comment) I think similar conclusions apply as topointwise?...? So the real question becomes what name to choose for the relation and its decidability, given thatLextakes three arguments -
<ₗₑₓ?: [ fix ]Relation.Nullary.Decidable.Corenames for combinators #2843 (comment) Ditto., but worth fixing the assumption names? [ fix ] assumption name inData.Product.Relation.Binary.Lex.Strict#2956
NB. The general situation for combinators is a bit mixed, both in their definition, and also in their use-sites, which might otherwise require some qualified name/renaming shenanigans to get things to work nicely. There is already an amount of that even in #2952 wrt ≡? vs. ≈? in order to disambiguate lemma statements. Sigh.
Reactions are currently unavailable
Metadata
Metadata
Assignees
Labels
No labels