pub proof fn seq_tracked_split_at<T>(tracked s: &mut Seq<T>, n: int) -> tracked result : Seq<T>Expand description
requires
0 <= n <= old(s).len(),*final(s) =~= old(s).subrange(0, n),result =~= old(s).subrange(n, old(s).len() as int),Splits a tracked sequence at position n, leaving [0, n) in s
and returning [n, len).