vstd::string

Function to_string_from_display_ensures_for_str

Source 
pub broadcast proof fn to_string_from_display_ensures_for_str(t: &str, res: String)
Expand description
ensures
#[trigger] to_string_from_display_ensures::<str>(t, res)
    <==> (t@ == res@ && t.is_ascii() == res.is_ascii()),