-
Notifications
You must be signed in to change notification settings - Fork 242
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add left- and right- Pointwise
congruence for _++_
on List
#2426
Conversation
Thanks @MatthewDaggitt : any opinions on the discussion points at the top? |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
While it would be nice to derive these through automation, we're kind of far from that. Let's have a full-featured library now, and worry about that later. So I'm all for merging this in.
I'm happy for old issues to still float around if they haven't been solved.
I think better that they exist first. We can then always refactor the implementation later. |
Have now added revised types for the new lemmas, and note the following:
Which nomenclature/notation should be taken as canon? (Potential issue: I think that the use(s) of left/right superscript annotations in the Barring the resolution of this question, I think this is (should be! ;-)) good to go now. |
Sigh as well. I think it's better to be consistent within |
Ok, I'll leave the names as is, but |
@JacquesCarette are you now happy with the revisions to this? |
Fixes #1131
NB: no
CHANGELOG
(yet), but adds:Data.List.Relation.Binary.Pointwise
Data.List.Relation.Binary.Equality.Setoid
Issue:
∙-congʳ
and∙-congˡ
for the(Is)Magma
structure/bundle defined onList
in Add theSetoid
-basedMonoid
on(List, [], _++_)
#2393 ...status:duplicate
and not merge after all (except perhaps the first pair of lemmas?)UPDATED: added
CHANGELOG
, and revised the types of lemmas in response to @JacquesCarette 's comments below.