Module vstd::pervasive

Macros

• struct_with_invariants
  Macro to help set up boilerplate for specifying invariants when using invariant-based datatypes.

Traits

• FnWithRequiresEnsures
• ForLoopGhostIterator
• ForLoopGhostIteratorNew
• VecAdditionalExecFns

Functions

• affirm
• arbitrary
• assert
• assume
• print_u64
• proof_from_false
• runtime_assert
• spec_affirm
• trigger
• unreached