Trait DeepModel 

pub trait DeepModel {
    type DeepModelTy;

    // Required method
    fn deep_model(self) -> Self::DeepModelTy;
}

The deep model corresponds to the model used for specifying operations such as equality, hash function or ordering, which are computed deeply in a data structure. Typically, such a model recursively calls deep models of inner types.

Required Associated Types

type DeepModelTy

Required Methods

fn deep_model(self) -> Self::DeepModelTy

logic

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementations on Foreign Types

impl DeepModel for ()

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

/* Macro-generated */

type DeepModelTy = ()

impl DeepModel for BigRational

Available on creusot and crate feature std only.

fn deep_model(self) -> Self::DeepModelTy

logic(opaque)

type DeepModelTy = Real

impl DeepModel for Duration

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.view()

type DeepModelTy = Int

impl DeepModel for Instant

Available on crate feature std only.

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.view()

type DeepModelTy = Int

impl DeepModel for Ordering

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self

type DeepModelTy = Ordering

impl DeepModel for String

Available on crate feature std only.

fn deep_model(self) -> Self::DeepModelTy

logic

type DeepModelTy = Seq<char>

impl DeepModel for bool

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self

type DeepModelTy = bool

impl DeepModel for char

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self@

type DeepModelTy = Int

impl DeepModel for i8

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self@

type DeepModelTy = Int

impl DeepModel for i16

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self@

type DeepModelTy = Int

impl DeepModel for i32

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self@

type DeepModelTy = Int

impl DeepModel for i64

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self@

type DeepModelTy = Int

impl DeepModel for i128

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self@

type DeepModelTy = Int

impl DeepModel for isize

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self@

type DeepModelTy = Int

impl DeepModel for str

fn deep_model(self) -> Self::DeepModelTy

logic

type DeepModelTy = Seq<char>

impl DeepModel for u8

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self@

type DeepModelTy = Int

impl DeepModel for u16

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self@

type DeepModelTy = Int

impl DeepModel for u32

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self@

type DeepModelTy = Int

impl DeepModel for u64

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self@

type DeepModelTy = Int

impl DeepModel for u128

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self@

type DeepModelTy = Int

impl DeepModel for usize

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self@

type DeepModelTy = Int

impl<A: DeepModel, Z: DeepModel, Y: DeepModel, X: DeepModel, W: DeepModel, V: DeepModel, U: DeepModel, T: DeepModel> DeepModel for (A, Z, Y, X, W, V, U, T)

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.$idx.deep_model(),

type DeepModelTy = (<A as DeepModel>::DeepModelTy, <Z as DeepModel>::DeepModelTy, <Y as DeepModel>::DeepModelTy, <X as DeepModel>::DeepModelTy, <W as DeepModel>::DeepModelTy, <V as DeepModel>::DeepModelTy, <U as DeepModel>::DeepModelTy, <T as DeepModel>::DeepModelTy)

impl<B: DeepModel, A: DeepModel, Z: DeepModel, Y: DeepModel, X: DeepModel, W: DeepModel, V: DeepModel, U: DeepModel, T: DeepModel> DeepModel for (B, A, Z, Y, X, W, V, U, T)

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.$idx.deep_model(),

type DeepModelTy = (<B as DeepModel>::DeepModelTy, <A as DeepModel>::DeepModelTy, <Z as DeepModel>::DeepModelTy, <Y as DeepModel>::DeepModelTy, <X as DeepModel>::DeepModelTy, <W as DeepModel>::DeepModelTy, <V as DeepModel>::DeepModelTy, <U as DeepModel>::DeepModelTy, <T as DeepModel>::DeepModelTy)

impl<C: DeepModel, B: DeepModel, A: DeepModel, Z: DeepModel, Y: DeepModel, X: DeepModel, W: DeepModel, V: DeepModel, U: DeepModel, T: DeepModel> DeepModel for (C, B, A, Z, Y, X, W, V, U, T)

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.$idx.deep_model(),

type DeepModelTy = (<C as DeepModel>::DeepModelTy, <B as DeepModel>::DeepModelTy, <A as DeepModel>::DeepModelTy, <Z as DeepModel>::DeepModelTy, <Y as DeepModel>::DeepModelTy, <X as DeepModel>::DeepModelTy, <W as DeepModel>::DeepModelTy, <V as DeepModel>::DeepModelTy, <U as DeepModel>::DeepModelTy, <T as DeepModel>::DeepModelTy)

impl<D: DeepModel, C: DeepModel, B: DeepModel, A: DeepModel, Z: DeepModel, Y: DeepModel, X: DeepModel, W: DeepModel, V: DeepModel, U: DeepModel, T: DeepModel> DeepModel for (D, C, B, A, Z, Y, X, W, V, U, T)

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.$idx.deep_model(),

type DeepModelTy = (<D as DeepModel>::DeepModelTy, <C as DeepModel>::DeepModelTy, <B as DeepModel>::DeepModelTy, <A as DeepModel>::DeepModelTy, <Z as DeepModel>::DeepModelTy, <Y as DeepModel>::DeepModelTy, <X as DeepModel>::DeepModelTy, <W as DeepModel>::DeepModelTy, <V as DeepModel>::DeepModelTy, <U as DeepModel>::DeepModelTy, <T as DeepModel>::DeepModelTy)

impl<E: DeepModel, D: DeepModel, C: DeepModel, B: DeepModel, A: DeepModel, Z: DeepModel, Y: DeepModel, X: DeepModel, W: DeepModel, V: DeepModel, U: DeepModel, T: DeepModel> DeepModel for (E, D, C, B, A, Z, Y, X, W, V, U, T)

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.$idx.deep_model(),

type DeepModelTy = (<E as DeepModel>::DeepModelTy, <D as DeepModel>::DeepModelTy, <C as DeepModel>::DeepModelTy, <B as DeepModel>::DeepModelTy, <A as DeepModel>::DeepModelTy, <Z as DeepModel>::DeepModelTy, <Y as DeepModel>::DeepModelTy, <X as DeepModel>::DeepModelTy, <W as DeepModel>::DeepModelTy, <V as DeepModel>::DeepModelTy, <U as DeepModel>::DeepModelTy, <T as DeepModel>::DeepModelTy)

impl<T: ?Sized> DeepModel for *const T

fn deep_model(self) -> Self::DeepModelTy

logic(opaque)

ensures

result.addr == self.addr_logic()

type DeepModelTy = PtrDeepModel

impl<T: ?Sized> DeepModel for *mut T

fn deep_model(self) -> Self::DeepModelTy

logic(opaque)

ensures

result.addr == self.addr_logic()

type DeepModelTy = PtrDeepModel

impl<T: ?Sized> DeepModel for NonNull<T>

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.view().deep_model()

type DeepModelTy = <*mut T as DeepModel>::DeepModelTy

impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Arc<T, A>

Available on crate feature nightly only.

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

*self.view().deep_model()

type DeepModelTy = <T as DeepModel>::DeepModelTy

impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Box<T, A>

Available on crate feature nightly only.

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

Box::new((*self).deep_model())

type DeepModelTy = Box<<T as DeepModel>::DeepModelTy>

impl<T: DeepModel + ?Sized, A: Allocator> DeepModel for Rc<T, A>

Available on crate feature nightly only.

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

*self.view().deep_model()

type DeepModelTy = <T as DeepModel>::DeepModelTy

impl<T: DeepModel + ?Sized> DeepModel for &T

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

(*self).deep_model()

type DeepModelTy = <T as DeepModel>::DeepModelTy

impl<T: DeepModel + ?Sized> DeepModel for &mut T

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

(*self).deep_model()

type DeepModelTy = <T as DeepModel>::DeepModelTy

impl<T: DeepModel, A: Allocator> DeepModel for Vec<T, A>

Available on crate feature nightly only.

fn deep_model(self) -> Self::DeepModelTy

logic(opaque)

ensures

self.view().len() == result.len()

ensures

forall<i> 0 <= i && i < self.view().len()
==> result[i] == self[i].deep_model()

type DeepModelTy = Seq<<T as DeepModel>::DeepModelTy>

impl<T: DeepModel, A: Allocator> DeepModel for VecDeque<T, A>

Available on crate feature nightly only.

fn deep_model(self) -> Self::DeepModelTy

logic(opaque)

ensures

self.view().len() == result.len()

ensures

forall<i> 0 <= i && i < self.view().len()
==> result[i] == self[i].deep_model()

type DeepModelTy = Seq<<T as DeepModel>::DeepModelTy>

impl<T: DeepModel, E: DeepModel> DeepModel for Result<T, E>

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

match self {
    Ok(t) => Ok(t.deep_model()),
    Err(e) => Err(e.deep_model()),
}

type DeepModelTy = Result<<T as DeepModel>::DeepModelTy, <E as DeepModel>::DeepModelTy>

impl<T: DeepModel, const N: usize> DeepModel for [T; N]

fn deep_model(self) -> Self::DeepModelTy

logic(opaque)

ensures

self.view().len() == result.len()

ensures

forall<i> 0 <= i && i < result.len() ==> result[i] == self[i].deep_model()

type DeepModelTy = Seq<<T as DeepModel>::DeepModelTy>

impl<T: DeepModel> DeepModel for (T,)

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.$idx.deep_model(),

type DeepModelTy = (<T as DeepModel>::DeepModelTy,)

impl<T: DeepModel> DeepModel for Bound<T>

fn deep_model(self) -> Self::DeepModelTy

logic(open)

match self {
    Bound::Included(b) => Bound::Included(b.deep_model()),
    Bound::Excluded(b) => Bound::Excluded(b.deep_model()),
    Bound::Unbounded => Bound::Unbounded,
}

type DeepModelTy = Bound<<T as DeepModel>::DeepModelTy>

impl<T: DeepModel> DeepModel for Option<T>

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

match self {
    Some(t) => Some(t.deep_model()),
    None => None,
}

type DeepModelTy = Option<<T as DeepModel>::DeepModelTy>

impl<T: DeepModel> DeepModel for Reverse<T>

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

Reverse(self.0.deep_model())

type DeepModelTy = Reverse<<T as DeepModel>::DeepModelTy>

impl<T: DeepModel> DeepModel for [T]

fn deep_model(self) -> Self::DeepModelTy

logic(opaque)

ensures

(&self)@.len() == result.len()

ensures

forall<i> 0 <= i && i < result.len() ==> result[i] == (&self)[i].deep_model()

type DeepModelTy = Seq<<T as DeepModel>::DeepModelTy>

impl<U: DeepModel, T: DeepModel> DeepModel for (U, T)

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.$idx.deep_model(),

type DeepModelTy = (<U as DeepModel>::DeepModelTy, <T as DeepModel>::DeepModelTy)

impl<V: DeepModel, U: DeepModel, T: DeepModel> DeepModel for (V, U, T)

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.$idx.deep_model(),

type DeepModelTy = (<V as DeepModel>::DeepModelTy, <U as DeepModel>::DeepModelTy, <T as DeepModel>::DeepModelTy)

impl<W: DeepModel, V: DeepModel, U: DeepModel, T: DeepModel> DeepModel for (W, V, U, T)

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.$idx.deep_model(),

type DeepModelTy = (<W as DeepModel>::DeepModelTy, <V as DeepModel>::DeepModelTy, <U as DeepModel>::DeepModelTy, <T as DeepModel>::DeepModelTy)

impl<X: DeepModel, W: DeepModel, V: DeepModel, U: DeepModel, T: DeepModel> DeepModel for (X, W, V, U, T)

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.$idx.deep_model(),

type DeepModelTy = (<X as DeepModel>::DeepModelTy, <W as DeepModel>::DeepModelTy, <V as DeepModel>::DeepModelTy, <U as DeepModel>::DeepModelTy, <T as DeepModel>::DeepModelTy)

impl<Y: DeepModel, X: DeepModel, W: DeepModel, V: DeepModel, U: DeepModel, T: DeepModel> DeepModel for (Y, X, W, V, U, T)

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.$idx.deep_model(),

type DeepModelTy = (<Y as DeepModel>::DeepModelTy, <X as DeepModel>::DeepModelTy, <W as DeepModel>::DeepModelTy, <V as DeepModel>::DeepModelTy, <U as DeepModel>::DeepModelTy, <T as DeepModel>::DeepModelTy)

impl<Z: DeepModel, Y: DeepModel, X: DeepModel, W: DeepModel, V: DeepModel, U: DeepModel, T: DeepModel> DeepModel for (Z, Y, X, W, V, U, T)

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self.$idx.deep_model(),

type DeepModelTy = (<Z as DeepModel>::DeepModelTy, <Y as DeepModel>::DeepModelTy, <X as DeepModel>::DeepModelTy, <W as DeepModel>::DeepModelTy, <V as DeepModel>::DeepModelTy, <U as DeepModel>::DeepModelTy, <T as DeepModel>::DeepModelTy)

Implementors

impl DeepModel for Id

type DeepModelTy = Id

impl DeepModel for Int

type DeepModelTy = Int

impl DeepModel for PeanoInt

type DeepModelTy = u64

impl<T: InhabitedInvariant + DeepModel> DeepModel for Subset<T>

type DeepModelTy = <T as DeepModel>::DeepModelTy