Function extern_spec_str_split_at 

pub fn extern_spec_str_split_at(self_: &str, ix: usize) -> (&str, &str)

extern spec for str::split_at

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

ghost

requires

self@.len() && self

ensures

self

ensures

result.0@.to_bytes().len() == ix@