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

fix: handle arguments and defaults consistently #16

Merged
merged 1 commit into from
Jan 10, 2025
Merged

Conversation

govereau
Copy link
Collaborator

@govereau govereau commented Jan 8, 2025

Default function arguments were not being handled the same way as function arguments. It was possible that an expression that could be passed as an argument could not have been used as a default value for the same argument. This patch fixes this issue, and simplifies some of the parsing code for arguments and function signatures.

Default function arguments were not being handled the same way as
function arguments. It was possible that an expression that could be
passed as an argument could not have been used as a default value for
the same argument. This patch fixes this issue, and simplifies some of
the parsing code for arguments and function signatures.
@govereau govereau added the bug Something isn't working label Jan 8, 2025
@govereau govereau requested a review from seanmcl January 8, 2025 11:06
@govereau govereau self-assigned this Jan 8, 2025
@govereau govereau requested a review from jtristan as a code owner January 8, 2025 11:06
@seanmcl
Copy link
Collaborator

seanmcl commented Jan 9, 2025

Could you give an example of

It was possible that an expression that could be passed as an argument could not have been used as a default value for the same argument.
?

NKL/Python.lean Show resolved Hide resolved
NKL/Python.lean Show resolved Hide resolved
NKL/Python.lean Show resolved Hide resolved
@govereau govereau merged commit 76e7364 into main Jan 10, 2025
1 check passed
@govereau govereau deleted the pg-defaults branch January 10, 2025 17:13
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants