Function extern_spec_Default_char_default 

pub fn extern_spec_Default_char_default() -> char

extern spec for char::default

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

terminates

ghost

ensures

result@ == 0