Attribute Macro creusot_contracts::macros::predicate

#[predicate]

Declare a function as being a predicate

This declaration must be pure and total. It cannot be called from Rust programs, but in exchange it can use logical operations and syntax with the help of the pearlite! macro.

It must return a boolean.

prophetic

If you wish to use the ^ operator on mutable borrows to get the final value, you need to specify that the function is prophetic, like so:

#[predicate(prophetic)]
fn uses_prophecies(x: &mut Int) -> bool {
    pearlite! { ^x == 0 }
}

Such a predicate function cannot be used in snapshot! anymore, and cannot be called from a regular logic or predicate function.