vstd

In vstd::prelude

Macros

atomic_with_ghost_helper
calc_proc_macro
decreases_to
decreases_to_internal
fndecl
proof
proof_decl
proof_with
struct_with_invariants
struct_with_invariants_vstd
verus
verus_erase_ghost
verus_exec_expr
verus_exec_expr_erase_ghost
verus_exec_expr_keep_ghost
verus_exec_inv_macro_exprs
verus_exec_macro_exprs
verus_ghost_inv_macro_exprs
verus_keep_ghost
verus_proof_expr
verus_proof_macro_explicit_exprs
verus_proof_macro_exprs
with_triggers

Structs

FnProof
FnSpec
Ghost
NoCopy
ProofFnConfirm
SpecChain
Tracked
int
nat

Constants

PROOF_FN
PROOF_FN_COPY
PROOF_FN_MUT
PROOF_FN_ONCE
PROOF_FN_SEND
PROOF_FN_SYNC

Traits

Boolean
Integer
ProofFn
ProofFnMut
ProofFnOnce
ProofFnReqEns
ProofFnReqEnsDef
SpecAdd
SpecBitAnd
SpecBitOr
SpecBitXor
SpecEuclideanDiv
SpecEuclideanMod
SpecMul
SpecNeg
SpecOrd
SpecShl
SpecShr
SpecSub
Structural

Functions

Attribute Macros

is_variant
is_variant_no_deprecation_warning
verus_enum_synthesize
verus_spec
verus_verify

Derive Macros

Structural

Function tracked_exec

Settings

Help

pub const fn tracked_exec<A>(_a: A) -> Tracked<A>