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

Unify definedness binders for function applications #4752

Open
Tracked by #4743
JuanCoRo opened this issue Feb 4, 2025 · 0 comments
Open
Tracked by #4743

Unify definedness binders for function applications #4752

JuanCoRo opened this issue Feb 4, 2025 · 0 comments

Comments

@JuanCoRo
Copy link
Member

JuanCoRo commented Feb 4, 2025

As per @tothtamas28:
When there are two identical function applications in a rule, separate binders for their definedness are generated.
It's possible that these two instances of the same application are not in the original KORE in this form, but through an alias.
The code generator inlines these aliases, so that's where the duplication might come from.

We could unify these definedness binders for ease of proving.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant