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

Support Apalache type-checking for specs with mutual recursion #14

Closed
Kukovec opened this issue Jul 22, 2024 · 1 comment
Closed

Support Apalache type-checking for specs with mutual recursion #14

Kukovec opened this issue Jul 22, 2024 · 1 comment
Assignees
@Kukovec

Comments

@Kukovec
Copy link
Contributor

Kukovec commented Jul 22, 2024

Unlike primitive recursion which, while not supported at the model-checking level, remains type-checkable, mutual recursion results in an error in the typechecking pass. (see #13 (comment))

We should introduce type-checking support for these operators as well.
@Kukovec Kukovec self-assigned this Jul 22, 2024
@Kukovec Kukovec changed the title Support typechecking specs with mutual recursion Support Apalache type-checking for specs with mutual recursion Jul 22, 2024
@konnov konnov mentioned this issue Sep 2, 2024
Open
@konnov
Copy link
Contributor

konnov commented Oct 2, 2024

See apalache-mc/apalache#2978

@konnov konnov closed this as completed Oct 2, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@Kukovec Kukovec

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@konnov @Kukovec