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

[ re #3423 ] Make IClaimData to be a data, not record #3465

Merged
merged 2 commits into from
Jan 15, 2025

Conversation

buzden
Copy link
Collaborator

@buzden buzden commented Jan 15, 2025

Description

PR #3423 introduces a new data structure which added several top-level declarations with names rig, vis, opts and type which leads a lot of existing code to warnings of shadowing these top-level names with local variables. These names are pretty popular, especially for parameter names in certain contexts (even precisely this module has already several parameters named in this way).

I believe that this was not the intended behaviour, to I suggest to declare IClaimData not as a record, like it's done with the type Record in the same module.

Pinging @andrevidela as the original PR author.

Copy link
Collaborator

@andrevidela andrevidela 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

@andrevidela andrevidela merged commit 393fb22 into idris-lang:main Jan 15, 2025
22 checks passed
@buzden buzden deleted the rename-opts branch January 15, 2025 13:51
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