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

sail-to-lean: fix implicit arguments #948

Open
javra opened this issue Feb 3, 2025 · 0 comments · May be fixed by #955
Open

sail-to-lean: fix implicit arguments #948

javra opened this issue Feb 3, 2025 · 0 comments · May be fixed by #955
Assignees
@javra
Labels
Lean Issues with Sail to Lean translation

Comments

@javra
Copy link
Collaborator

javra commented Feb 3, 2025

We mark an argument to a function as explicit if it's "shadowed" by a type level variable. But we don't distinguish between explicit and implicit ones when treating E_app, so we need to store implicitness in the environment.
@javra javra self-assigned this Feb 3, 2025
@tobiasgrosser tobiasgrosser added the Lean Issues with Sail to Lean translation label Feb 3, 2025
@javra javra linked a pull request Feb 4, 2025 that will close this issue
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@javra javra

Labels
Lean Issues with Sail to Lean translation
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Lean: support for implicit arguments in function application javra/sail
2 participants
@javra @tobiasgrosser