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

vstd/
prelude.rs
