Module 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

allow_panic

arbitrary

assert

assume

cloned

print_u64

proof_from_false

runtime_assert

spec_affirm

strictly_cloned

trigger

unreached