Skip to content

[ new ] updateAt and extra Properties on List.All #540

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

Closed
wants to merge 14 commits into from

Conversation

ajrouvoet
Copy link
Contributor

@ajrouvoet ajrouvoet commented Nov 22, 2018

New operations on List.All

@ajrouvoet ajrouvoet changed the title WIP [ new ] append and updateAt on List.All WIP [ new ] updateAt and extra Properties on List.All Nov 23, 2018
@ajrouvoet
Copy link
Contributor Author

For the properties of updateAt the "equal at point" relation defined by @andreasabel was useful again. So this PR depends on #510.

@ajrouvoet ajrouvoet changed the title WIP [ new ] updateAt and extra Properties on List.All [ new ] updateAt and extra Properties on List.All Nov 23, 2018
@gallais gallais added the status: blocked-by-issue Progress on this issue or PR is blocked by another issue. label Dec 16, 2018
@gallais gallais removed the status: blocked-by-issue Progress on this issue or PR is blocked by another issue. label Dec 25, 2018
@gallais
Copy link
Member

gallais commented Dec 25, 2018

The "equal at point" relation has been removed from #510.

@andreasabel
Copy link
Member

I hope this PR gets merged soon.
The All.updateAt operation is very useful, I need it all the time.

@MatthewDaggitt MatthewDaggitt modified the milestones: 1.0, v0.18 Jan 19, 2019
@MatthewDaggitt
Copy link
Contributor

Okay, we'll make sure to include in the next release.

@MatthewDaggitt
Copy link
Contributor

MatthewDaggitt commented Feb 22, 2019

I'm really confused about this PR. Somewhere along the line its actual content has got lost. Wasn't it supposed to add lemmas to Data.All.Properties?

Apologies @ajrouvoet could you perhaps open a new PR? I think the problem with this one was that @andreasabel 's that you based it on was modified quite a lot before it got merged.

@gallais
Copy link
Member

gallais commented Feb 22, 2019

This merge seems to be the culprit: because Data.List.All had moved,
git happily ignored the modifications made to it! 😭

@MatthewDaggitt MatthewDaggitt modified the milestones: v0.18, v1.0 Feb 22, 2019
@ajrouvoet
Copy link
Contributor Author

@MatthewDaggitt Yeah, it was maybe too ambitious to make a PR staged on another PR :) I can definitely make a new PR, but it is going to be after the ICFP deadline on March 1st

@MatthewDaggitt
Copy link
Contributor

MatthewDaggitt commented Feb 22, 2019

@MatthewDaggitt Yeah, it was maybe too ambitious to make a PR staged on another PR :) I can definitely make a new PR, but it is going to be after the ICFP deadline on March 1st

Okay thanks, that would be great! I'll leave this open until you do so.

@MatthewDaggitt
Copy link
Contributor

Superseded by #655

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
addition status: won't-merge Decided against merging the PR in.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants