Function vstd::compute::all_spec_implies
source · pub broadcast proof fn all_spec_implies(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)),