Quantifiers documentation is wrong

[carolynzech]

I tried this code from the quantifiers documentation:

#[kani::proof]
fn test_forall() {
    let v = vec![10; 10];
    kani::assert(kani::forall!(|i in 0..10| v[i] == 10));
}

using the following command line invocation:

cargo kani -Z function-contracts

with Kani version: 0.62.0

I expected to see this happen: verification success

Instead, this happened: explanation

error[E0061]: this function takes 2 arguments but 1 argument was supplied
  --> src/lib.rs:24:5
   |
24 |     kani::assert(kani::forall!(|i in 0..10| v[i] == 10));
   |     ^^^^^^^^^^^^---------------------------------------- argument #2 of type `&'static str` is missing
   |
note: function defined here
  --> /Users/cmzech/kani/library/kani/src/lib.rs:55:1
   |
55 | kani_core::kani_lib!(kani);
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^
   = note: this error originates in the macro `kani_core::kani_intrinsics` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info)
help: provide the argument
   |
24 |     kani::assert(kani::forall!(|i in 0..10| v[i] == 10), /* &'static str */);
   |                                                        ++++++++++++++++++++

I added a message, then got this error:

Kani Rust Verifier 0.62.0 (cargo plugin)
   Compiling playground v0.1.0 (/Users/cmzech/playground)
error: no rules expected `0`
  --> src/lib.rs:24:38
   |
24 |     kani::assert(kani::forall!(|i in 0..10| v[i] == 10), "msg");
   |                                      ^ no rules expected this token in macro call
   |
note: while trying to match `(`
  --> /Users/cmzech/kani/library/kani/src/lib.rs:55:1
   |
55 | kani_core::kani_lib!(kani);
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^
   = note: this error originates in the macro `kani_core::kani_intrinsics` which comes from the expansion of the macro `kani_core::kani_lib` (in Nightly builds, run with -Z macro-backtrace for more info)

I got this to work:

#[kani::proof]
fn test_forall() {
    let v = vec![10; 10];
    kani::assert(kani::forall!(|i in (0,10)| v[i] == 10), "msg");
}

So we should update our documentation and RFC to match the syntax we actually support.