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.

Sign up for GitHub

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

Jump to bottom

Rename homo to ∙-homo in Algebra.Morphism.Structures #2464

Open
wants to merge 8 commits into
base: master
Choose a base branch
from
Open

Rename homo to ∙-homo in Algebra.Morphism.Structures #2464

wants to merge 8 commits into from

Conversation

jamesmckinna
Copy link
Contributor

@jamesmckinna jamesmckinna commented Aug 29, 2024 •
edited
Loading

Fixes #2458

NB: the warning-on-usage does not seem to be correctly triggering when reference to homo is made in renaming directives, nor in actual usage? UPDATED: A known, but not-yet-fixed, Agda bug. Grrrr.

JacquesCarette
JacquesCarette approved these changes Aug 29, 2024
View reviewed changes
Copy link
Contributor

@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 to me - but isn't this a breaking change?

@jamesmckinna jamesmckinna added this to the v2.2 milestone Aug 29, 2024
@jamesmckinna
Copy link
Contributor Author

jamesmckinna commented Aug 29, 2024 •
edited
Loading

Looks good to me - but isn't this a breaking change?

I forget (or: have never properly understood?!) whether changing (field) names via deprecation is breaking or not?
UPDATED: Oh, I suppose it must be!?

@jamesmckinna jamesmckinna modified the milestones: v2.2, v3.0 Aug 29, 2024
This was referenced Aug 29, 2024
Open
Open
@MatthewDaggitt
Copy link
Contributor

Yes, unfortunately it is an unavoidable breaking change.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@JacquesCarette JacquesCarette JacquesCarette approved these changes

@MatthewDaggitt MatthewDaggitt Awaiting requested review from MatthewDaggitt

Assignees
No one assigned
Labels
breaking cosmetic deprecation naming refactoring
Projects
None yet
Milestone
v3.0
Development

Successfully merging this pull request may close these issues.

Get rid of inconsistent homo name in algebra hierarchy?
3 participants
@jamesmckinna @MatthewDaggitt @JacquesCarette