vstd/
prelude.rs

1#[cfg(not(verus_verify_core))]
2pub use verus_builtin::*;
3
4#[cfg(verus_verify_core)]
5pub use crate::verus_builtin::*;
6
7// Omit contrib macros from the following list; they are exported in contrib/mod.rs
8pub use verus_builtin_macros::atomic_with_ghost_helper;
9pub use verus_builtin_macros::calc_proc_macro;
10pub use verus_builtin_macros::fndecl;
11pub use verus_builtin_macros::is_variant;
12pub use verus_builtin_macros::is_variant_no_deprecation_warning;
13pub use verus_builtin_macros::proof;
14pub use verus_builtin_macros::proof_decl;
15pub use verus_builtin_macros::proof_with;
16pub use verus_builtin_macros::struct_with_invariants;
17pub use verus_builtin_macros::verus;
18pub use verus_builtin_macros::verus_enum_synthesize;
19pub use verus_builtin_macros::verus_erase_ghost;
20pub use verus_builtin_macros::verus_exec_expr;
21pub use verus_builtin_macros::verus_exec_expr_erase_ghost;
22pub use verus_builtin_macros::verus_exec_expr_keep_ghost;
23pub use verus_builtin_macros::verus_exec_inv_macro_exprs;
24pub use verus_builtin_macros::verus_exec_macro_exprs;
25pub use verus_builtin_macros::verus_ghost_inv_macro_exprs;
26pub use verus_builtin_macros::verus_impl;
27pub use verus_builtin_macros::verus_keep_ghost;
28pub use verus_builtin_macros::verus_proof_expr;
29pub use verus_builtin_macros::verus_proof_macro_explicit_exprs;
30pub use verus_builtin_macros::verus_proof_macro_exprs;
31pub use verus_builtin_macros::verus_spec;
32pub use verus_builtin_macros::verus_trait_impl;
33pub use verus_builtin_macros::verus_verify;
34pub use verus_builtin_macros::Structural;
35pub use verus_builtin_macros::StructuralEq;
36
37pub use super::map::map;
38pub use super::map::Map;
39pub use super::seq::seq;
40pub use super::seq::Seq;
41pub use super::set::set;
42pub use super::set::Set;
43pub use super::view::*;
44
45#[cfg(verus_keep_ghost)]
46pub use super::pervasive::{affirm, arbitrary, cloned, proof_from_false, spec_affirm, unreached};
47
48pub use super::array::ArrayAdditionalExecFns;
49pub use super::array::ArrayAdditionalSpecFns;
50#[cfg(verus_keep_ghost)]
51pub use super::pervasive::FnWithRequiresEnsures;
52pub use super::slice::SliceAdditionalSpecFns;
53#[cfg(verus_keep_ghost)]
54pub use super::std_specs::option::OptionAdditionalFns;
55#[cfg(verus_keep_ghost)]
56pub use super::std_specs::result::ResultAdditionalSpecFns;
57
58#[cfg(verus_keep_ghost)]
59#[cfg(feature = "alloc")]
60pub use super::std_specs::vec::VecAdditionalSpecFns;
61
62#[cfg(feature = "alloc")]
63pub use super::pervasive::VecAdditionalExecFns;
64
65pub use super::string::StrSliceExecFns;
66#[cfg(feature = "alloc")]
67pub use super::string::StringExecFns;
68#[cfg(feature = "alloc")]
69pub use super::string::StringExecFnsIsAscii;
70
71#[cfg(verus_keep_ghost)]
72pub use super::tokens::CountToken;
73#[cfg(verus_keep_ghost)]
74pub use super::tokens::ElementToken;
75#[cfg(verus_keep_ghost)]
76pub use super::tokens::KeyValueToken;
77#[cfg(verus_keep_ghost)]
78pub use super::tokens::MonotonicCountToken;
79#[cfg(verus_keep_ghost)]
80pub use super::tokens::SimpleToken;
81#[cfg(verus_keep_ghost)]
82pub use super::tokens::ValueToken;
83
84#[cfg(verus_keep_ghost)]
85pub use super::tokens::InstanceId;
vstd/prelude.rs

vstd/
prelude.rs
