Function vstd::seq_lib::subrange_of_matching_take

source · 
pub proof fn subrange_of_matching_take<T>(
    a: Seq<T>,
    b: Seq<T>,
    s: int,
    e: int,
    l: int
)
Expand description
requires
a.take(l) == b.take(l),
l <= a.len(),
l <= b.len(),
0 <= s <= e <= l,
ensures
a.subrange(s, e) == b.subrange(s, e),