We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
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
In the current version, exceptional post-conditions are represented with the type : (xsymbol * (pattern * term) list) list
(xsymbol * (pattern * term) list) list
This doesn't work well with exception that doesn't have any arguments. For example in:
exception E val f : int -> int (*@ y = f x raises E -> x = 42
the type checker has to fill for the pattern. It wil linsert a tuple0 pattern, I believe because the type of E is Exn_tuple [].
tuple0
E
Exn_tuple []
The text was updated successfully, but these errors were encountered:
After further investigation, the tuple0 is placed by the parser. In case we have a pattern but no term (raises E _), the parser will insert a Ttrue.
raises E _
Ttrue
I believe there are two ways to go:
(xsymbol * pattern option * term) list
(pattern * term) list
Sorry, something went wrong.
No branches or pull requests
In the current version, exceptional post-conditions are represented with the type :
(xsymbol * (pattern * term) list) list
This doesn't work well with exception that doesn't have any arguments. For example in:
the type checker has to fill for the pattern.
It wil linsert a
tuple0
pattern, I believe because the type ofE
isExn_tuple []
.The text was updated successfully, but these errors were encountered: