Trait creusot_contracts::resolve::Resolve

pub trait Resolve {
    // Required methods
    fn resolve(self) -> bool;
    fn resolve_coherence(&self);
}

Required Methods

fn resolve(self) -> bool

logic(prophetic)

fn resolve_coherence(&self)

logic(prophetic)

requires

inv(self)

requires

structural_resolve(self)

ensures

(*self).resolve()

Implementations on Foreign Types

impl<T1, T2: ?Sized> Resolve for (T1, T2)

fn resolve(self) -> bool

logic(prophetic)

resolve(&self.0) && resolve(&self.1)

fn resolve_coherence(&self)

logic(prophetic)

{}

requires

structural_resolve(self)

ensures

(*self).resolve()

impl<T: ?Sized> Resolve for &mut T

fn resolve(self) -> bool

logic(prophetic)

pearlite! { ^self == *self }

fn resolve_coherence(&self)

logic(prophetic)

{}

requires

structural_resolve(self)

ensures

(*self).resolve()

Implementors

impl<'a, T> Resolve for IterMut<'a, T>

impl<I> Resolve for Cloned<I>

impl<I> Resolve for Copied<I>

impl<I> Resolve for Enumerate<I>

impl<I> Resolve for Skip<I>

impl<I> Resolve for Take<I>

impl<I, B, F> Resolve for MapInv<I, B, F>

impl<I, F> Resolve for Map<I, F>

impl<T> Resolve for Option<T>

impl<T> Resolve for VecDeque<T>

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

impl<T, A: Allocator> Resolve for IntoIter<T, A>

impl<T: ?Sized> Resolve for GhostBox<T>

impl<T: ?Sized> Resolve for Box<T>