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

Convert quint record operators #2530

Closed
shonfeder opened this issue Apr 12, 2023 · 0 comments · Fixed by #2535
Closed

Convert quint record operators #2530

shonfeder opened this issue Apr 12, 2023 · 0 comments · Fixed by #2535
Assignees
@shonfeder
Labels
feature A new feature or functionality
Milestone
Transpile Apalach...

Comments

@shonfeder
Copy link
Contributor

These were missed in the initial planning because they are not enumerated in the reference I was using to draw up the plans.

I should be able to use https://github.com/informalsystems/quint/blob/186d24cac62599ef60056475204521467fdead14/doc/lang.md#L1248-L1263
@shonfeder shonfeder added the feature A new feature or functionality label Apr 12, 2023
@shonfeder shonfeder self-assigned this Apr 12, 2023
@shonfeder shonfeder changed the title Convert quint record operator Convert quint record operators Apr 12, 2023
This was referenced Apr 14, 2023
Merged
Closed
@apalache-bot apalache-bot mentioned this issue Apr 17, 2023
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@shonfeder shonfeder

Labels
feature A new feature or functionality
Projects
None yet
Milestone
Transpile ApalacheIR from QuintAST
Development

Successfully merging a pull request may close this issue.

Convert quint record operators apalache-mc/apalache
1 participant
@shonfeder