Module creusot_contracts::prelude

Re-exports

• pub use crate::ghost::GhostBox;
• pub use crate::logic::ops::IndexLogic as _;
• pub use crate::logic::Int;
• pub use crate::logic::OrdLogic;
• pub use crate::logic::Seq;
• pub use crate::model::DeepModel;
• pub use crate::model::View;
• pub use crate::snapshot::Snapshot;
• pub use crate::std::default::Default;
• pub use crate::std::iter::FromIterator;
• pub use crate::std::iter::IntoIterator;
• pub use crate::std::iter::Iterator;
• pub use crate::well_founded::WellFounded;
• 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::ptr::PointerExt as _;
• pub use crate::std::slice::SliceExt as _;
• pub use crate::util::such_that;
• pub use crate::resolve::*;
• pub use crate::macros::*;

Traits

• Clone
  A common trait for the ability to explicitly duplicate an object.
• PartialEq
  Trait for comparisons using the equality operator.

Derive Macros

• Clone
• DeepModel
• Default
  Derive macro generating an impl of the trait Default.
• PartialEq