Trait vstd::compute::RangeAll

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

Simplify proofs-by-computation for ranges of values

Required Methods§

source

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.

Object Safety§

This trait is not object safe.

Implementations on Foreign Types§

source§

impl RangeAll for Range<int>

source§

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

{ range_all_spec_rec(self, p) }

Implementors§