creusot_contracts::std::iter

Trait FusedIterator

Source 
pub trait FusedIterator: FusedIterator + Iterator {
    // Required method
    fn is_fused(&mut self, steps: Seq<Self::Item>, next: Self);
}

Required Methods§

Source

fn is_fused(&mut self, steps: Seq<Self::Item>, next: Self)

law

requires 

self.completed()

requires 

(^self).produces(steps, next)

ensures 

steps == Seq::EMPTY && ^self == next

Dyn Compatibility§

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors§