vstd
In vstd::
prelude
Macros
atomic_with_ghost_helper
calc_proc_macro
decreases_to
decreases_to_internal
fndecl
proof
proof_decl
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
FnSpec
Ghost
NoCopy
SpecChain
Tracked
int
nat
Traits
Boolean
Integer
SpecAdd
SpecBitAnd
SpecBitOr
SpecBitXor
SpecEuclideanDiv
SpecEuclideanMod
SpecMul
SpecNeg
SpecOrd
SpecShl
SpecShr
SpecSub
Structural
Functions
add
admit
arch_word_bits
array_index
assert_
assert_bit_vector
assert_bitvector_by
assert_by
assert_by_compute
assert_by_compute_only
assert_forall_by
assert_nonlinear_by
assume_
call_ensures
call_requires
choose
choose_tuple
closure_to_fn_spec
decreases
decreases_by
decreases_when
ensures
equal
exists
ext_equal
ext_equal_deep
extra_dependency
forall
get_union_field
get_variant_field
ghost_exec
global_size_of
imply
infer_spec_for_loop_iter
inline_air_stmt
invariant
invariant_except_break
is_smaller_than
is_smaller_than_lexicographic
is_smaller_than_recursive_function_field
is_variant
mul
no_method_body
no_unwind
no_unwind_when
old
opens_invariants
opens_invariants_any
opens_invariants_except
opens_invariants_none
opens_invariants_set
recommends
recommends_by
requires
returns
reveal_hide_
reveal_hide_internal_path_
reveal_strlit
signed_max
signed_min
spec_cast_integer
spec_chained_cmp
spec_chained_eq
spec_chained_ge
spec_chained_gt
spec_chained_le
spec_chained_lt
spec_chained_value
spec_eq
spec_literal_int
spec_literal_integer
spec_literal_nat
strslice_get_char
strslice_is_ascii
strslice_len
sub
tracked_exec
tracked_exec_borrow
unsigned_max
use_type_invariant
with_triggers
Attribute Macros
is_variant
is_variant_no_deprecation_warning
verus_enum_synthesize
verus_spec
verus_verify
Derive Macros
Structural
?
Settings
Macro
vstd
::
prelude
::
proof
Copy item path
[
−
]
proof!() {
/* proc-macro */
}
Expand description
Add a verus proof block.