List of all items

Macros

• extern_spec
• ghost
• pearlite
• proof_assert
• snapshot

Attribute Macros

• bitwise_proof
• ensures
• invariant
• law
• logic
• maintains
• open
• open_inv_result
• predicate
• pure
• requires
• terminates
• trusted
• variant

Derive Macros

• DeepModel
• Resolve