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.

terminates

ghost

requires

exists<i0> 0 <= i0 && i0 <= self@.len() && self@.subsequence(0, i0).to_bytes().len() == ix@

ensures

result.0@.concat(result.1@) == self@

ensures

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