8000 Don't print generalized parameters in helper functions by knisht · Pull Request #6689 · agda/agda · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Don't print generalized parameters in helper functions #6689

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
Merged
merged 3 commits into from
Jun 15, 2023
Merged

Don't print generalized parameters in helper functions #6689

merged 3 commits into from
Jun 15, 2023

Conversation

knisht
Copy link
Contributor
@knisht knisht commented Jun 11, 2023 •
edited
Loading

Fixes #6677.
I could not find any way to get the number of generalized arguments for a meta, so I had to add this functionality.
It seems bad that the semantics of defArgGeneralizable becomes multi-purpose, but it looks suitable for carrying this kind of information.

Zurihac intensifies...

@andreasabel andreasabel added the ux: generate helper Generation of helper function type signatures (C-c C-h) label Jun 14, 2023
@andreasabel andreasabel added this to the 2.6.4 milestone Jun 14, 2023
andreasabel
andreasabel approved these changes Jun 14, 2023
View reviewed changes
Copy link
Member
@andreasabel andreasabel left a comment

Choose a reason for hiding this comment

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

Great, thanks!

Could you add a sentence to the CHANGELOG.

@andreasabel
Copy link
Member
8000

I extended the existing changelog entry for helper functions to the current feature.

@andreasabel andreasabel self-assigned this Jun 15, 2023
@andreasabel andreasabel merged commit b7f4c7d into agda:master Jun 15, 2023
@andreasabel andreasabel mentioned this pull request Sep 13, 2023
Closed
@knisht knisht mentioned this pull request Sep 16, 2023
Closed
@andreasabel andreasabel mentioned this pull request Feb 7, 2024
Closed
JobPetrovcic pushed a commit to JobPetrovcic/agda that referenced this pull request Apr 12, 2024
@andreasabel @JobPetrovcic
Changelog for agda#6689
cbbe8b6
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@andreasabel andreasabel andreasabel approved these changes

Assignees

@andreasabel andreasabel

Labels
ux: generate helper Generation of helper function type signatures (C-c C-h)
Projects
None yet
Milestone
2.6.4
Development

Successfully merging this pull request may close these issues.

Helper function type includes generalized parameters
2 participants
@knisht @andreasabel
0