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

[Refactor] imports to use Relation.Nullary.Irrelevant #2676

Merged
merged 7 commits into from
Mar 23, 2025
Merged

[Refactor] imports to use Relation.Nullary.Irrelevant #2676

merged 7 commits into from
Mar 23, 2025

Conversation

jmougeot
Copy link
Contributor

@jmougeot jmougeot commented Mar 14, 2025 •
edited
Loading

Update imports to replace references to Relation.Nullary with Relation.Nullary.Irrelevant where applicable, enhancing clarity and organization in the codebase. #2624

Taneb
Taneb requested changes Mar 14, 2025
View reviewed changes
Copy link
Member

@Taneb Taneb left a comment

Choose a reason for hiding this comment

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

There's a new module, so there should be a changelog entry

@jmougeot
Copy link
Contributor Author

jmougeot commented Mar 14, 2025 •
edited
Loading

I just added the changelog entry, but I’m not sure if I did it correctly.

@jamesmckinna jamesmckinna mentioned this pull request Mar 15, 2025
Merged
@jamesmckinna
Copy link
Contributor

Also a good idea, for the sake of the GitHub history, to explicitly mention #2624 , which this now does over as a 'clean' PR.

jamesmckinna
jamesmckinna requested changes Mar 15, 2025
View reviewed changes
Copy link
Contributor

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

Besides the nitpick, I am now convinced about the benefits of the refactoring, esp. wrt removing the imports with hiding (Irrelevant) directives.

JacquesCarette
JacquesCarette requested changes Mar 15, 2025
View reviewed changes
@jmougeot jmougeot changed the title Refactor imports to use Relation.Nullary.Irrelevant [Refactor] imports to use Relation.Nullary.Irrelevant #2624 Mar 17, 2025
@jmougeot jmougeot changed the title [Refactor] imports to use Relation.Nullary.Irrelevant #2624 [Refactor] imports to use Relation.Nullary.Irrelevant Mar 17, 2025
jamesmckinna
jamesmckinna approved these changes Mar 17, 2025
View reviewed changes
Copy link
Contributor

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

Suggested tweak, but optional.

@jmougeot @jamesmckinna
Update CHANGELOG.md
38b1824 
Co-authored-by: jamesmckinna <[email protected]>
@jamesmckinna
Copy link
Contributor

@Taneb @JacquesCarette are either/both of you happy now? Suggest clearing this one off the docket?

@JacquesCarette JacquesCarette added this pull request to the merge queue Mar 23, 2025
Merged via the queue into agda:master with commit 4871f37 Mar 23, 2025
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Taneb Taneb Taneb approved these changes

@JacquesCarette JacquesCarette JacquesCarette approved these changes

@jamesmckinna jamesmckinna jamesmckinna approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@jmougeot @jamesmckinna @JacquesCarette @Taneb