Skip to content
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 a constructor to the Category interface #3483

Merged
merged 1 commit into from
Feb 3, 2025

Conversation

andrevidela
Copy link
Collaborator

Description

Adding constructors to category interface

We should probably also move this outside contrib, maybe have other things that are categories to go along with it

Should this change go in the CHANGELOG?

  • If this is a fix, user-facing change, a compiler change, or a new paper
    implementation, I have updated CHANGELOG_NEXT.md (and potentially also
    CONTRIBUTORS.md).

@andrevidela andrevidela marked this pull request as ready for review February 3, 2025 17:49
@andrevidela andrevidela merged commit 0751a91 into main Feb 3, 2025
46 checks passed
@buzden
Copy link
Collaborator

buzden commented Feb 3, 2025

We should probably also move this outside contrib, maybe have other things that are categories to go along with it

I'm working on a proposition of a change in interfaces elaboration that would allow this interface and arrows interface to be more usable. I'm not suggesting waiting for it, but I definitely would for moving all these things out of contrib after my work is finished

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants