Function vstd::seq_lib::lemma_seq_take_len

source · 
pub proof fn lemma_seq_take_len<A>(s: Seq<A>, n: int)
Expand description
ensures
0 <= n <= s.len() ==> s.take(n).len() == n,

Taking the first n elements of a sequence results in a sequence of length n, as long as n is within the bounds of the original sequence.