List of all items

Macros

• declare_namespace
• extern_spec
• ghost
• ghost_let
• pearlite
• proof_assert
• snapshot

Attribute Macros

• bitwise_proof
• builtin
• check
• ensures
• erasure
• intrinsic
• invariant
• logic
• maintains
• opaque
• open_inv_result
• requires
• trusted
• variant

Derive Macros

• DeepModel