Function extern_spec_core_slice_from_ref 

pub fn extern_spec_core_slice_from_ref<T>(s: &T) -> &[T]

extern spec for ::core::slice::from_ref<T>

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

terminates

ghost

ensures

result@.len() == 1

ensures

result@[0] == *s