Skip to content

[ add ] missing Function.Bundles#3069

Merged
jamesmckinna merged 7 commits into
agda:masterfrom
jamesmckinna:missing-function-bundles
Jul 15, 2026
Merged

[ add ] missing Function.Bundles#3069
jamesmckinna merged 7 commits into
agda:masterfrom
jamesmckinna:missing-function-bundles

Conversation

@jamesmckinna

Copy link
Copy Markdown
Collaborator

Fixes #2229 ? The orphaned commit identified on that issue seems simply never to have had a PR raised against it... until now.

Only open question is about the knock-on deprecations... not sure what's needed, so reviewer(s) please note!

@MatthewDaggitt MatthewDaggitt 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.

Looks good to me! I'm not sure what deprecations would be needed? These kind of additions don't usually result in deprecations.

@JacquesCarette JacquesCarette 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.

I agree with @MatthewDaggitt -- which means you ought to modify the CHANGELOG.

Comment thread CHANGELOG.md Outdated
@jamesmckinna

jamesmckinna commented Jul 14, 2026

Copy link
Copy Markdown
Collaborator Author

Looks good to me! I'm not sure what deprecations would be needed? These kind of additions don't usually result in deprecations.

So... I have now installed deprecations, because the code has moved... and indeed, given the sheer amount of re-duplication/re-export, possibly more could be deprecated, eg Function.Properties.Inverse.Inverse⇒Equivalence, or even... all of the conversions after the successful merge of #2583 ? For now, I've focused only on those in the OP...

Further comments/review welcome on these decisions! See also (and perhaps reopen!?) #2570 ... or move such discussion to #3070

@jamesmckinna
jamesmckinna added this pull request to the merge queue Jul 15, 2026
Merged via the queue into agda:master with commit 339d7a6 Jul 15, 2026
13 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Missing reexports in function bundles

4 participants