Attribute Macro creusot_contracts::macros::requires

#[requires]

A pre-condition of a function or trait item

The inside of a requires may look like Rust code, but it is in fact pearlite.

Example

#[requires(x@ == 1)]
fn foo(x: i32) {}