Function extern_spec_core_iter_once 

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

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

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

terminates

ghost

ensures

result@ == Some(value)