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

Move raw bundles from Data.X.Properties to Data.X.Base #1810

Merged
merged 6 commits into from
Oct 6, 2022
Merged

Move raw bundles from Data.X.Properties to Data.X.Base #1810

merged 6 commits into from
Oct 6, 2022

Conversation

5xy1
Copy link
Contributor

@5xy1 5xy1 commented Sep 1, 2022 •
edited by MatthewDaggitt
Loading

fixes #1755

@JacquesCarette JacquesCarette mentioned this pull request Sep 1, 2022
Closed
@MatthewDaggitt MatthewDaggitt added this to the v2.0 milestone Sep 5, 2022
@MatthewDaggitt
Copy link
Contributor

Thanks @5xy1! There's a discussion going on in #1755 about whether we should move the definitions of the raw bundles themselves to Algebra.Bundles.Raw, will keep you updated about the resolution.

@Taneb
Copy link
Member

Taneb commented Sep 20, 2022

@5xy1 if you're up to it, could you also move RawLattice from Algebra.Lattice.Bundles to a new module Algebra.Lattice.Bundles.Raw?

@5xy1
Copy link
Contributor Author

5xy1 commented Sep 20, 2022

@Taneb Of course, I'd be happy to! I might update this PR tonight.

MatthewDaggitt
MatthewDaggitt reviewed Sep 23, 2022
View reviewed changes
Copy link
Contributor

@MatthewDaggitt MatthewDaggitt left a comment

Choose a reason for hiding this comment

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

Thanks, looks great! Just a few more small comments and then it'll be ready to merge!

@MatthewDaggitt
Copy link
Contributor

Ooh also @5xy1 we'll need to update README.Design.Heirarchies with an entry for Bundles.Raw. Do you think you could do so? Happy to do it otherwise if you're not comfortable with doing so.

@5xy1
Copy link
Contributor Author

5xy1 commented Sep 26, 2022

@MatthewDaggitt I'm afraid of missing something, so I would be grateful if you could do it!

@MatthewDaggitt MatthewDaggitt merged commit 578e7a6 into agda:master Oct 6, 2022
This was referenced Oct 24, 2022
Closed
Closed
@jamesmckinna jamesmckinna mentioned this pull request Feb 2, 2023
Closed
@andreasabel andreasabel mentioned this pull request Jul 24, 2023
Merged
@andreasabel andreasabel mentioned this pull request Aug 27, 2023
Merged
@andreasabel andreasabel mentioned this pull request Oct 12, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@MatthewDaggitt MatthewDaggitt MatthewDaggitt left review comments

Assignees
No one assigned
Labels
refactoring
Projects
None yet
Milestone
v2.0
Development

Successfully merging this pull request may close these issues.

Move "raw" bundles to Data.X.Base
3 participants
@5xy1 @MatthewDaggitt @Taneb