Function extern_spec_T_NonZero_T_new_unchecked 

pub unsafe fn extern_spec_T_NonZero_T_new_unchecked<T: ZeroablePrimitive + View<ViewTy = Int>>(
    n: T,
) -> NonZero<T>

extern spec for NonZero<T>::new_unchecked

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

requires

n@ != 0

ensures

result.get_logic() == n

ghost