Macro cvlr_predicate 

macro_rules! cvlr_predicate {
    (| $c:ident : $ctx: ident | -> { $($body:tt)* } ) => { ... };
}

Creates an anonymous predicate (boolean expression) over a context type.

This macro creates an anonymous predicate that implements CvlrFormula for the specified context type. Unlike cvlr_def_predicate!, this macro creates an unnamed predicate that can be used inline without defining a separate type.

Syntax

cvlr_predicate! {
    | <context_var> : <context_type> | -> {
        <expression1>;
        <expression2>;
        ...
    }
}

Parameters

• context_var - The variable name to use for the context in the predicate body
• context_type - The type of the context
• expressions - One or more expressions that form the predicate body

Returns

Returns a value implementing CvlrFormula with Context = Ctx that can be evaluated, asserted, or assumed.

Examples

use cvlr_spec::cvlr_predicate;

struct Counter {
    value: i32,
}

let ctx = Counter { value: 5 };

// Create an anonymous predicate
let pred = cvlr_predicate! { | c : Counter | -> {
    c.value > 0;
    c.value < 100
} };

assert!(pred.eval(&ctx));

Note: This example is marked ignore because it doesn’t require special setup. In actual usage, predicates are often used within lemmas or other verification contexts.

This macro is often used internally by [cvlr_lemma!] to create the requires and ensures predicates.