Open vfukala opened 11 months ago
The eventual syntax will be closure!( #[requires(..)] |..| .. )
to match method annotations. However, the various closure features are still put on hold and I'm not sure I'll get to merging these before the Prusti rewrite.
Are there some closure features that already partially work (possibly somewhere on another branch)?
In the user guide, in the section about closures, the (only) example
fails to compile with
The user guide says to see PR #138 for the status of closures as a Prusti feature and that the syntax for adding specs to closures currently doesn't work. The examples I found in the PR fail to compile with similar errors. The PR was merged back in 2020.
So I'm a bit confused if closure specification works at all anywhere? If I can use it Prusti in any way?