Consider adding error-codes #641
jaybosamiya
started this conversation in
General
Replies: 1 comment
-
My suggestion wrt the format itself would be to just use the format that Rust uses, i.e. Another alternative is to use |
Beta Was this translation helpful? Give feedback.
0 replies
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
-
It would be useful for us to have each error reported by Verus come with an error code, similar to Rust (see https://doc.rust-lang.org/stable/error_codes/error-index.html).
This would allow users who face an error to quickly look-up more details, or easily jump to relevant part of code in Verus, and so on. Also, it would help create a point for documentation to build on, for example get more hints on ways to fix up the error and such.
Opening this as a separate discussion from #387 since that one focuses on the specific error messages itself, but this is about updating all error codes.
Beta Was this translation helpful? Give feedback.
All reactions