Function extern_spec_str_is_ascii 

pub fn extern_spec_str_is_ascii(self_: &str) -> bool

extern spec for str::is_ascii

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

ghost

ensures

result == (forall<i> i >= 0 && i < self@.len() ==> self@[i]@ <= 127)