Function extern_spec_core_str_from_utf8_unchecked 

pub unsafe fn extern_spec_core_str_from_utf8_unchecked(bytes: &[u8]) -> &str

extern spec for ::core::str::from_utf8_unchecked

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

ghost

requires

exists<s: Seq<char>> s.to_bytes() == bytes@

ensures

result@.to_bytes() == bytes@