Skip to content

Add properties relating Vec.lookup to head and tail#3004

Open
Taneb wants to merge 6 commits into
masterfrom
vec-lookup-head-tail
Open

Add properties relating Vec.lookup to head and tail#3004
Taneb wants to merge 6 commits into
masterfrom
vec-lookup-head-tail

Conversation

@Taneb

@Taneb Taneb commented Jun 8, 2026

Copy link
Copy Markdown
Member

Really surprised these didn't already exist!

@jamesmckinna jamesmckinna left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

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

Happy enough with things as they are here, but with some questions to at least consider.

Also: CHANGELOG

Comment thread src/Data/Vec/Properties.agda Outdated
Comment thread src/Data/Vec/Properties.agda Outdated
Comment thread src/Data/Vec/Properties.agda Outdated
@Taneb

Taneb commented Jun 9, 2026

Copy link
Copy Markdown
Member Author

I'm holding off adding a changelog for this and my other PRs until after 2.4 is released

@jamesmckinna

Copy link
Copy Markdown
Collaborator

I'm holding off adding a changelog for this and my other PRs until after 2.4 is released

Yeah, but this is such low-hanging fruit that it could easily be a v2.4 contribution?

@MatthewDaggitt

Copy link
Copy Markdown
Collaborator

We've already made a release candidate for v2.4 and I'm very reluctant to add anything else to it.

Comment thread CHANGELOG.md Outdated
Comment thread CHANGELOG.md Outdated
@jamesmckinna

Copy link
Copy Markdown
Collaborator

A couple of additional comments on CHANGELOG, after which I'd be happy to hit merge...

Comment thread src/Data/Vec/Properties.agda Outdated
@Taneb Taneb requested a review from JacquesCarette June 15, 2026 12:42
@jamesmckinna

Copy link
Copy Markdown
Collaborator

This all looks good to me now, so I'll enable auto-merge so that if @JacquesCarette toggles his review to Accept, then we can put this to bed.

@jamesmckinna jamesmckinna enabled auto-merge June 15, 2026 13:18
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.

5 participants