Function vstd::compute::all_spec_ensures

source · 
pub broadcast proof fn all_spec_ensures(r: Range<int>, p: FnSpec<(int,), bool>)
Expand description
ensures
#[trigger] r.all_spec(p) ==> (forall |i| r.start <= i < r.end ==> #[trigger] p(i)),