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

feat: add the ability to access the uncurried base #37

Merged
merged 3 commits into from
Aug 17, 2024
Merged

feat: add the ability to access the uncurried base #37

merged 3 commits into from
Aug 17, 2024

Conversation

Equilibris
Copy link
Collaborator

Currently, we only expose the curried Base functor for each given type, this limits how we are able to extend the Base functor and would limit adding DeepThunks to the code as these require the uncurried Base functor

AtticusKuhn
AtticusKuhn reviewed Aug 16, 2024
View reviewed changes
Copy link
Contributor

@AtticusKuhn AtticusKuhn 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. I like how this PR is nice and small.
I don't really understand the full context of why DeepThunk requires uncurried functors, but as long as you do, that's fine.

alexkeizer
alexkeizer approved these changes Aug 16, 2024
View reviewed changes
Copy link
Owner

@alexkeizer alexkeizer left a comment

Choose a reason for hiding this comment

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

LGTM

Qpf/Macro/Data.lean Outdated Show resolved Hide resolved
@Equilibris @alexkeizer
Update Qpf/Macro/Data.lean
633e2c0 
Co-authored-by: Alex Keizer <alex@keizer.dev>
@Equilibris Equilibris merged commit b490634 into master Aug 17, 2024
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@AtticusKuhn AtticusKuhn AtticusKuhn left review comments

@alexkeizer alexkeizer alexkeizer 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.
3 participants
@Equilibris @alexkeizer @AtticusKuhn