List of all items

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