Macro cvlr_def_predicate 

macro_rules! cvlr_def_predicate {
    (pred $name: ident ( $c:ident : $ctx: ident ) {  $( $e: expr );* $(;)? }) => { ... };
}

Defines a predicate (boolean expression) over a context type.

This macro creates a new type implementing [CvlrFormula] for the specified context. The predicate body consists of one or more expressions that are evaluated, asserted, or assumed together.

Syntax

cvlr_def_predicate! {
    pred <name> ( <context_var> : <context_type> ) {
        <expression1>;
        <expression2>;
        ...
    }
}

Parameters

• name - The name of the predicate type to create
• 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

Examples

use cvlr_spec::cvlr_def_predicate;

struct MyContext {
    x: i32,
    y: i32,
}

cvlr_def_predicate! {
    pred IsPositive ( c : MyContext ) {
        c.x > 0;
        c.y > 0;
    }
}

let ctx = MyContext { x: 5, y: 10 };
let pred = IsPositive;
assert!(pred.eval(&ctx));