Function extern_spec_T_NonZero_T_new 

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

extern spec for NonZero<T>::new

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

ensures

match result {
    None => n@ == 0,
    Some(nz) => n@ != 0 && nz.get_logic() == n,
}

ghost