Function vstd::string::axiom_str_literal_get_char

source · 
pub broadcast proof fn axiom_str_literal_get_char<'a>(s: &'a str, i: int)
Expand description
ensures
#[trigger] s@.index(i) == strslice_get_char(s, i),