Attribute Macro prusti_contracts::requires

source ·
#[requires]
Expand description

A macro for writing a precondition on a function.