Function extern_spec_std_iter_once 

pub fn extern_spec_std_iter_once<T>(value: T) -> Once<T>

extern spec for ::std::iter::once<T>

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

terminates

ghost

ensures

result@ == Some(value)