Expand description
Re-exports available under the creusot_contracts namespace
Re-exports§
pub use crate::ghost::Ghost;pub use crate::invariant::Invariant;pub use crate::logic::Int;pub use crate::logic::OrdLogic;pub use crate::logic::Seq;pub use crate::logic::ops::IndexLogic as _;pub use crate::model::DeepModel;pub use crate::model::View;pub use crate::resolve::Resolve;pub use crate::snapshot::Snapshot;pub use crate::std::iter::DoubleEndedIteratorSpec;pub use crate::std::iter::FromIteratorSpec;pub use crate::std::iter::IteratorSpec;pub use crate::std::vec::vec;pub use crate::std::char::CharExt as _;pub use crate::std::iter::SkipExt as _;pub use crate::std::iter::TakeExt as _;pub use crate::std::ops::FnExt as _;pub use crate::std::ops::FnMutExt as _;pub use crate::std::ops::FnOnceExt as _;pub use crate::std::ops::RangeInclusiveExt as _;pub use crate::std::option::OptionExt as _;pub use crate::std::ptr::PointerExt as _;pub use crate::std::ptr::SizedPointerExt as _;pub use crate::std::ptr::SlicePointerExt as _;pub use crate::std::slice::SliceExt as _;pub use crate::invariant::inv;pub use crate::resolve::resolve;pub use crate::macros::*;