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

Deduplicate definitions #1022

Merged
merged 24 commits into from
Feb 7, 2024
Merged

Deduplicate definitions #1022

merged 24 commits into from
Feb 7, 2024

Conversation

fredrik-bakke
Copy link
Collaborator

Resolves #992.

@fredrik-bakke
Copy link
Collaborator Author

gotta fix the rest of the names in reflection tomorrow.

@fredrik-bakke
Copy link
Collaborator Author

Turns out constructor names can be overloaded. I.e. two different inductive types can have constructors with the same name. Did you guys know this?

@EgbertRijke
Copy link
Collaborator

I did not know this, but I don't want us to exploit this in agda-unimath

@EgbertRijke
Copy link
Collaborator

Perhaps for records I did know this

@fredrik-bakke
Copy link
Collaborator Author

agreed, I was just a bit shocked to find out

@fredrik-bakke
Copy link
Collaborator Author

For context, constructor overloading was used in reflection. I'm working to disambiguate them now.

@EgbertRijke
Copy link
Collaborator

Awesome! Thank you for taking care of that part of the library

@fredrik-bakke
Copy link
Collaborator Author

Okay, this one is ready for review now. Note that it does not do a complete refactor of reflection, although it improves on many of its bad practices. I did not want to touch group-solver in the end because it is such a hot mess.

@fredrik-bakke fredrik-bakke marked this pull request as ready for review February 7, 2024 11:03
EgbertRijke
EgbertRijke approved these changes Feb 7, 2024
View reviewed changes
Copy link
Collaborator

@EgbertRijke EgbertRijke left a comment

Choose a reason for hiding this comment

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

Thank you for making this PR. I think I had only one small comment, so we can merge it soon.

@fredrik-bakke
Copy link
Collaborator Author

Done! :)

@EgbertRijke EgbertRijke merged commit 9d6df60 into UniMath:master Feb 7, 2024
4 checks passed
@fredrik-bakke fredrik-bakke deleted the duplicates branch March 28, 2024 14:20
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@EgbertRijke EgbertRijke EgbertRijke approved these changes

Assignees
No one assigned
Labels
CI finite-algebra finite-group-theory refactoring reflection
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Resolve duplicate definitions
2 participants
@fredrik-bakke @EgbertRijke