Function vstd::string::axiom_str_literal_is_ascii
source · pub broadcast proof fn axiom_str_literal_is_ascii<'a>(s: &'a str)Expand description
ensures
#[trigger] s.is_ascii() == strslice_is_ascii(s),