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.

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

Generalize types of inspect idiom #1041

Merged
merged 1 commit into from
Sep 15, 2023

Conversation

dolio
Copy link
Contributor

@dolio dolio commented Sep 4, 2023

This generalizes some types to allow doing an inspect of a dependent function. I've found myself wanting this from time to time, and I haven't noticed the generalization having any adverse effects (I think the fact that f is an argument nails down potential ambiguities about B).

Copy link
Collaborator

@mortberg mortberg left a comment

Choose a reason for hiding this comment

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

Seems like a reasonable change that I can merge directly. Thanks for the contribution!

@mortberg mortberg merged commit 3202e38 into agda:master Sep 15, 2023
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants