vstd::std_specs::vec

Function axiom_spec_len

Source 
pub broadcast proof fn axiom_spec_len<A>(v: &Vec<A>)
Expand description
ensures
#[trigger] spec_vec_len(v) == v@.len(),