Crate prusti_contracts_proc_macros 

Macros

body_invariant

body_variant

ghost

predicate

prusti_assert

prusti_assume

prusti_refute

Attribute Macros

after_expiry

assert_on_expiry

ensures

extern_spec

invariant

model

print_counterexample

pure

refine_spec

refine_trait_spec

requires

terminates

trusted

verified