Trait RangeAll 

pub trait RangeAll
where
    Self: Sized,
{
    // Required method
    spec fn all_spec(self, p: FnSpec<(int,), bool>) -> bool;
}

Simplify proofs-by-computation for ranges of values

Required Methods

spec fn all_spec(self, p: FnSpec<(int,), bool>) -> bool

Checks whether p holds for all values in this range. See the Verus tutorial for example usage.

Dyn Compatibility

This trait is not dyn compatible.

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

Implementations on Foreign Types

impl RangeAll for Range<int>

open spec fn all_spec(self, p: FnSpec<(int,), bool>) -> bool

{ range_all_spec_rec(self, p) }

Implementors