vstd::string

Function axiom_str_literal_len

Source 
pub broadcast proof fn axiom_str_literal_len<'a>(s: &'a str)
Expand description
ensures
#[trigger] s@.len() == strslice_len(s),