(Documentation of) Closures

[vfukala]

In the user guide, in the section about closures, the (only) example

use prusti_contracts::*;

fn main() {
    let cl = closure!(
        requires(a > b),
        ensures(result > b),
        |a: i32, b: i32| -> i32 { a }
    );
}

fails to compile with

  __          __        __  ___             
 |__)  _\/_  |__) |  | /__`  |   ____\/_  | 
 |      /\   |  \ \__/ .__/  |       /\   | 

Prusti version: 0.2.2, commit 5486c19e14e 2023-07-20 19:49:27 UTC, built on 2023-07-24 13:29:48 UTC
error: expected `|`
 --> clo.rs:5:9
  |
5 |         requires(a > b),
  |         ^^^^^^^^

error: aborting due to previous error

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?

[Aurel300]

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.

[vfukala]

Are there some closure features that already partially work (possibly somewhere on another branch)?