Skip to content

Support for checking types, constants, params#13

Merged
daniel-larraz merged 3 commits intokind2-mc:mainfrom
Jabe03:constant-info
Apr 10, 2026
Merged

Support for checking types, constants, params#13
daniel-larraz merged 3 commits intokind2-mc:mainfrom
Jabe03:constant-info

Conversation

@Jabe03
Copy link
Copy Markdown
Contributor

@Jabe03 Jabe03 commented Apr 8, 2026

Added:

  • Distinction between constants and parameters
  • Can now construct a call to Kind 2 that uses the --lus_main_const flag

Dependencies:

  • This PR is dependent on PR #20 of the Java API and PR #44 of the VS Code extenstion
    • It uses the new main constant flag (API) and the signatures of check, realizability, and minimalCutSet have new interfaces to the VS Code extension

@Jabe03
Copy link
Copy Markdown
Contributor Author

Jabe03 commented Apr 8, 2026

Note: the build is failing since GitHub does not have the new version of the Kind 2 LSP

@daniel-larraz daniel-larraz merged commit ecda375 into kind2-mc:main Apr 10, 2026
1 check passed
daniel-larraz pushed a commit to kind2-mc/vscode-kind2 that referenced this pull request Apr 10, 2026
Added:
- Constants now have check and check realizability, while params now
have just check realizability
- When calling LSP, now distinguished between `nodeDecl`, `paramDecl`,
`constDecl`, and `typeDecl`

Dependencies:
- This change depends on PR
[#13](kind2-mc/kind2-language-server#13) of the
LSP
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants