Skip to content

[ new ] map-concat#2453

Merged
jamesmckinna merged 1 commit intoagda:masterfrom
gallais:map-concat
Aug 2, 2024
Merged

[ new ] map-concat#2453
jamesmckinna merged 1 commit intoagda:masterfrom
gallais:map-concat

Conversation

@gallais
Copy link
Member

@gallais gallais commented Aug 1, 2024

Preparing next year's coursework and I'll need this. :)

Copy link
Collaborator

@JacquesCarette JacquesCarette left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looks good.

Makes me sad that concat isn't defined in terms of fold so that this could become a special case of map-fold. Ah well.

@jamesmckinna
Copy link
Collaborator

Looks good.

Makes me sad that concat isn't defined in terms of fold so that this could become a special case of map-fold. Ah well.

Two things

So: possible issue (v3.0? hypothetical-rewrite?) to systematically refactor the whole lot?

@jamesmckinna jamesmckinna added this to the v2.2 milestone Aug 1, 2024
Copy link
Collaborator

@jamesmckinna jamesmckinna left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Aaargh... my previous Approve was too hasty...

@jamesmckinna jamesmckinna dismissed their stale review August 1, 2024 10:41

sheer idiocy/over-hasty reviewing

Copy link
Collaborator

@jamesmckinna jamesmckinna left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Third time's the charm...

@jamesmckinna jamesmckinna added this pull request to the merge queue Aug 2, 2024
Merged via the queue into agda:master with commit 7e9e14a Aug 2, 2024
@gallais gallais deleted the map-concat branch August 2, 2024 12:22
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants