vstd
In vstd::
std_
specs::
vec
vstd
::
std_specs
::
vec
Function
axiom_spec_len
Copy item path
Source
pub
broadcast proof
fn axiom_spec_len<A>(v: &
Vec
<A>)
Expand description
ensures
#[trigger]
spec_vec_len(v) == v@.len(),