vstd::compute

Function range_all_spec_rec

Source 
pub open spec fn range_all_spec_rec(r: Range<int>, p: FnSpec<(int,), bool>) -> bool
Expand description
{
    if r.start >= r.end {
        true
    } else {
        p(r.start) && range_all_spec_rec(r.start + 1..r.end, p)
    }
}