Modules§
Macros§
- parse_
quote_ spanned - Same as
parse_quote!, but applies a given span to all tokens originating within the macro invocation.
Enums§
- Extern
Spec Kind - Spec
Attribute Kind - This type identifies one of the procedural macro attributes of Prusti
Constants§
Functions§
- body_
invariant - body_
variant - closure
- extern_
spec - ghost
- invariant
- predicate
- print_
counterexample - prusti_
assertion - prusti_
assume - prusti_
refutation - refine_
trait_ spec - rewrite_
prusti_ attributes - Rewrite an item as required by all its specification attributes.
- rewrite_
prusti_ attributes_ for_ types - trusted
- type_
model