Function extern_spec_From_String_Box_str_from 

pub fn extern_spec_From_String_Box_str_from(s: String) -> Box<str>

extern spec for Box<str>::from

This is not a real function: its only use is for documentation.

ghost

ensures

result@ == s@