Re-exports§
pub use super::map::map;pub use super::map::Map;pub use super::seq::seq;pub use super::seq::Seq;pub use super::set::set;pub use super::set::Set;pub use super::pervasive::affirm;pub use super::pervasive::arbitrary;pub use super::pervasive::proof_from_false;pub use super::pervasive::spec_affirm;pub use super::pervasive::unreached;pub use super::array::ArrayAdditionalExecFns;pub use super::array::ArrayAdditionalSpecFns;pub use super::pervasive::FnWithRequiresEnsures;pub use super::slice::SliceAdditionalSpecFns;pub use super::std_specs::option::OptionAdditionalFns;pub use super::std_specs::result::ResultAdditionalSpecFns;pub use super::std_specs::vec::VecAdditionalSpecFns;pub use super::pervasive::VecAdditionalExecFns;pub use super::string::StrSliceExecFns;pub use super::string::StringExecFns;pub use super::string::StringExecFnsIsAscii;pub use super::tokens::CountToken;pub use super::tokens::ElementToken;pub use super::tokens::KeyValueToken;pub use super::tokens::MonotonicCountToken;pub use super::tokens::SimpleToken;pub use super::tokens::ValueToken;pub use super::tokens::InstanceId;pub use super::view::*;
Macros§
- decreases_to!(b => a) means that height(a) < height(b), so that b can decrease to a in decreases clauses. decreases_to!(b1, …, bn => a1, …, am) can compare lexicographically ordered values, which can be useful when making assertions about decreases clauses. Notes:
verus_proof_macro_explicit_exprs!(f!(tts))applies verus syntax to transformttsintotts', then returnsf!(tts'), only applying the transform to any of the exprs within it that are explicitly prefixed with@@, leaving the rest as-is. Contrast this to [verus_proof_macro_exprs] which is likely what you want to try first to see if it satisfies your needs.- verus_proof_macro_exprs!(f!(exprs)) applies verus syntax to transform exprs into exprs’, then returns f!(exprs’), where exprs is a sequence of expressions separated by “,”, “;”, and/or “=>”.