Macro creusot_contracts::macros::pearlite

pearlite!() { /* proc-macro */ }

Enables pearlite syntax, granting access to Pearlite specific operators and syntax

This is meant to be used in logic functions.

Example

#[predicate]
fn all_ones(s: Seq<Int>) -> bool {
    // Allow access to `forall` and `==>` among other things
    pearlite! {
        forall<i: Int> 0 <= i && i < s.len() ==> s[i] == 1
    }
}