-
Notifications
You must be signed in to change notification settings - Fork 22
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 issue #57 and probably #51 #60
Conversation
Finally, we have a new restriction where a free variable on the left should be applied to the same number of argument. However, this PR is not ready to be merged, since @Gaspi will clean the code. |
kernel/rule.ml
Outdated
|
||
More precisely: | ||
- Context variables are exclusively applied to distinct locally bound variables | ||
- Occurences of such variable are all applied to the same number of arguments |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I would say "Occurences of each context variable" instead of "Occurences of such variable".
@Gaspi I think this PR is ready to be merged. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I agree that it's time to merge it.
Replace a min by a max.