Requested feature: Improve UX for ensure clauses.
Use case: Since #3207, ensures are now represented as closures that receive a reference of the return value. However, when using this annotation, we often get an error that requires the type to be specified.
Link to relevant documentation (Rust reference, Nomicon, RFC):
error[E0282]: type annotations needed
--> promoted_constants_enum.rs:16:18
|
16 | #[kani::ensures(|result| *result == Foo::A)]
| ^^^^^^ ------- type must be known at this point
|
help: consider giving this closure parameter an explicit type
|
16 | #[kani::ensures(|result: /* Type */| *result == Foo::A)]
Requested feature: Improve UX for ensure clauses. Use case: Since #3207, ensures are now represented as closures that receive a reference of the return value. However, when using this annotation, we often get an error that requires the type to be specified. Link to relevant documentation (Rust reference, Nomicon, RFC):
Test case:
I get the following compilation error: